module Cat.Instances.Graphs.Representable where

Representable graphs🔗

We define the representable graphs, those which correspond to representable functors under the equivalence between the category of graphs and presheaves over the parallel arrows diagram.

The node graph is the graph with a single node and no edges.

Nodeᴳ : Graph lzero lzero
Nodeᴳ .Node     = 
Nodeᴳ .Edge _ _ = 
Nodeᴳ .Node-set = hlevel 2
Nodeᴳ .Edge-set = hlevel 2

The edge graph is the graph with a single edge, and the necessary pair of nodes to support it.

Edgeᴳ : Graph lzero lzero
Edgeᴳ .Node = Bool
Edgeᴳ .Edge = Edgeᵉ
Edgeᴳ .Node-set = hlevel 2
Edgeᴳ .Edge-set = hlevel 2

The edge graph must have a pair of nodes because our definition of graphs defines edges only over the source and target; alternatively, in a fibred presentation, it is because edges must have an image under the source and target maps, and these can be distinct (and so must be in a representing object). Thinking about the equivalence with presheaves, these two nodes correspond to the two maps in the parallel arrows diagram.

As the names imply, morphisms from these “shape” graphs correspond to picking out the corresponding structure in some other graph: either a node or an edge.

node→hom : G .Node  Graph-hom Nodeᴳ G
node→hom x .node tt = x
node→hom x .edge ()

edge→hom :  {x y}  G .Edge x y  Graph-hom Edgeᴳ G
edge→hom {x = x} {y} e .node false = x
edge→hom {x = x} {y} e .node true  = y
edge→hom e .edge inc = e

Monomorphisms of graphs🔗

As an application of these graphs, we can show that monomorphisms of graphs are componentwise embeddings of the node and edge sets. This will be useful in constructing the subgraph classifier. In both cases, this is proved by evaluating the monomorphism at morphisms which represent the nodes and edges we are comparing.

module _ {m : Graphs.Hom G H} (monic : Graphs.is-monic m) where
  is-monic→node-is-embedding : is-embedding (m .node)
  is-monic→node-is-embedding = injective→is-embedding! λ p  monic {c = Liftᴳ _ _ Nodeᴳ}
    record { node = _ ; edge = λ () }
    record { node = _ ; edge = λ () }
    (Graph-hom-path  _  p)  ()))
    ·ₚ lift tt

  is-monic→edge-is-embedding :  {x y}  is-embedding (m .edge {x} {y})
  is-monic→edge-is-embedding = injective→is-embedding! λ {x} {y} p 
    let
      a = monic {c = Liftᴳ _ _ Edgeᴳ} (edge→hom x ∘ᴳ lowerᴳ) (edge→hom y ∘ᴳ lowerᴳ) $ ext λ where
        .node true   refl
        .node false  refl
        .edge (lift inc)  p

      px = ap  m  m .node (lift false)) a
      py = ap  m  m .node (lift true)) a

      b : subst₂ (G .Edge) px py x  y
      b = from-pathp (ap  m  m .edge (lift inc)) a)
    in sym (transport-refl _)
      subst₂  α β  subst₂ (G .Edge) α β x  y) prop! prop! b