module Cat.Instances.Graphs where

The category of graphs🔗

A graph (really, an 1) is given by a set of nodes and, for each pair of elements a set of edges from to That’s it: a set and a family of sets over

record Graph (o  : Level) : Type (lsuc o  lsuc ) where
  no-eta-equality
  field
    Node : Type o
    Edge : Node  Node  Type 

    Node-set : is-set Node
    Edge-set :  {x y}  is-set (Edge x y)

A graph homomorphism consists of a mapping of nodes along with a mapping of edges

record Graph-hom (G : Graph o ) (H : Graph o' ℓ') : Type (o  o'    ℓ') where
  no-eta-equality
  field
    node :  G    H 
    edge :  {x y}  G .Edge x y  H .Edge (node x) (node y)
{-# INLINE Graph-hom.constructor #-}
private variable
  G H K : Graph o 

open Graph-hom

unquoteDecl H-Level-Graph-hom = declare-record-hlevel 2 H-Level-Graph-hom (quote Graph-hom)

instance
  Funlike-Graph-hom : Funlike (Graph-hom G H)  G  λ _   H 
  Funlike-Graph-hom .Funlike._·_ = node

Graph-hom-pathp
  : {G : I  Graph o } {H : I  Graph o' ℓ'}
   {f : Graph-hom (G i0) (H i0)} {g : Graph-hom (G i1) (H i1)}
   (p0 :  (x :  i  G i .Node)
           PathP  i  H i .Node)
              (f · x i0) (g · x i1))
   (p1 :  {x y :  i  G i .Node}
           (e :  i  G i .Edge (x i) (y i))
           PathP  i  H i .Edge (p0 x i) (p0 y i))
              (f .edge (e i0)) (g .edge (e i1)))
   PathP  i  Graph-hom (G i) (H i)) f g
Graph-hom-pathp {G = G} {H = H} {f = f} {g = g} p0 p1 = pathp where
  node* : I  Type _
  node* i = (G i) .Node

  edge* : (i : I)  node* i  node* i  Type _
  edge* i x y = (G i) .Edge x y

  pathp : PathP  i  Graph-hom (G i) (H i)) f g
  pathp i .node x = p0  j  coe node* i j x) i
  pathp i .edge {x} {y} e =
    p1 {x = λ j  coe node* i j x} {y = λ j  coe node* i j y}
       j  coe  j  edge* j (coe node* i j x) (coe node* i j y)) i j (e* j)) i
    where

      x* y* : (j : I)  node* i
      x* j = coei→i node* i x (~ j  i)
      y* j = coei→i node* i y (~ j  i)

      e* : (j : I)  edge* i (coe node* i i x) (coe node* i i y)
      e* j =
        comp  j  edge* i (x* j) (y* j)) (I-eq i j) λ where
          k (k = i0)  e
          k (i = i0) (j = i0)  e
          k (i = i1) (j = i1)  e

Graph-hom-path
  : {f g : Graph-hom G H}
   (p0 :  x  f .node x  g .node x)
   (p1 :  {x y}  (e : Graph.Edge G x y)  PathP  i  Graph.Edge H (p0 x i) (p0 y i)) (f .edge e) (g .edge e))
   f  g
Graph-hom-path {G = G} {H = H} p0 p1 =
  Graph-hom-pathp {G = λ _  G} {H = λ _  H}
     x i  p0 (x i) i)
     e i  p1 (e i) i)

module _ {o o'  ℓ' ℓr} {G : Graph o } {H : Graph o' ℓ'}  rel : Extensional ( G    H ) ℓr  where
  record Graph-hom∼ (f g : Graph-hom G H) : Type (o  o'    ℓ'  ℓr) where
    field
      node : rel .Pathᵉ (f .node) (g .node)
      edge
        :  {x y} (e : G .Edge x y)
         PathP  i  H .Edge (rel .idsᵉ .to-path node i x) (rel .idsᵉ .to-path node i y))
            (f .edge {x} {y} e) (g .edge {x} {y} e)

  open Graph-hom∼ public

  private unquoteDecl eqv = declare-record-iso eqv (quote Graph-hom∼)

  instance
    Extensional-graph-hom : Extensional (Graph-hom G H) (o  o'    ℓ'  ℓr)
    Extensional-graph-hom .Pathᵉ = Graph-hom∼
    Extensional-graph-hom .reflᵉ x .node   = rel .reflᵉ (x .node)
    Extensional-graph-hom .reflᵉ x .edge {a} {b} e = to-pathp
      (ap₂  α β  subst₂ (H .Edge) {b' = x .node b} α β (x .edge e))
         i j  to-path-refl {a = x .node} (rel .idsᵉ) i j · a)
         i j  to-path-refl {a = x .node} (rel .idsᵉ) i j · b)
       transport-refl _)
    Extensional-graph-hom .idsᵉ .to-path p i .node = rel .idsᵉ .to-path (p .node) i
    Extensional-graph-hom .idsᵉ .to-path p i .edge e = p .edge e i
    Extensional-graph-hom .idsᵉ .to-path-over p = is-prop→pathp
       i  Iso→is-hlevel 1 eqv (Σ-is-hlevel 1
        (Equiv→is-hlevel 1 (identity-system-gives-path (rel .idsᵉ)) (hlevel 1))
         x  hlevel 1)))
      _ _

macro
  trivialᴳ! : Term  TC 
  trivialᴳ! goal = unify goal (def (quote Graph-hom-path) (lam visible (abs "_" (def (quote refl) [])) v∷ lam visible (abs "_" (def (quote refl) [])) v∷ []))

idᴳ : {G : Graph o }  Graph-hom G G
idᴳ .node v = v
idᴳ .edge e = e

_∘ᴳ_ :  {G : Graph o } {H : Graph o' ℓ'} {I : Graph o'' ℓ''}
   Graph-hom H I  Graph-hom G H  Graph-hom G I
(f ∘ᴳ h) .node x = f .node (h .node x)
(f ∘ᴳ h) .edge x = f .edge (h .edge x)

Graphs and graph homomorphisms can be organized into a category

Graphs :  o   Precategory (lsuc (o  )) (o  )
Graphs o  .Precategory.Ob = Graph o 
Graphs o  .Precategory.Hom = Graph-hom
Graphs o  .Precategory.Hom-set _ _ = hlevel 2
Graphs o  .Precategory.id  = idᴳ
Graphs o  .Precategory._∘_ = _∘ᴳ_
Graphs o  .Precategory.idr _ = trivialᴳ!
Graphs o  .Precategory.idl _ = trivialᴳ!
Graphs o  .Precategory.assoc _ _ _ = trivialᴳ!
open Functor
open _=>_
module _ {o  : Level} where
  module Graphs = Cat.Reasoning (Graphs o )

  graph-iso-is-ff : {x y : Graph o } (h : Graphs.Hom x y)  Graphs.is-invertible h   {x y}  is-equiv (h .edge {x} {y})
  graph-iso-is-ff {x} {y} h inv {s} {t} = is-iso→is-equiv (iso from ir il) where
    module h = Graphs.is-invertible inv

    from :  {s t}  y .Edge (h · s) (h · t)  x .Edge s t
    from e = subst₂ (x .Edge) (ap node h.invr · _) (ap node h.invr · _) (h.inv .edge e)

    ir : is-right-inverse from (h .edge)
    ir e =
      h .edge (subst₂ (x .Edge) _ _ (h.inv .edge e))
        ≡˘⟨ subst₂-fibrewise {C' = λ a b  y .Edge (h .node a) (h .node b)}  _ _  h .edge) _ _ _ ≡˘
      subst₂ (y .Edge) _ _ (h .edge (h.inv .edge e))
        ≡⟨ ap₂  a b  subst₂ (y .Edge) {b' = h .node t} a b (h .edge (h.inv .edge e))) prop! prop! 
      subst₂ (y .Edge) _ _ (h .edge (h.inv .edge e))
        ≡⟨ from-pathp  i  h.invl i .edge e) 
      e 

    il : is-left-inverse from (h .edge)
    il e = from-pathp λ i  h.invr i .edge e

  Graph-path
    :  {x y : Graph o }
     (p : x .Node  y .Node)
     (PathP  i  p i  p i  Type ) (x .Edge) (y .Edge))
     x  y
  Graph-path {x = x} {y} p q i .Node = p i
  Graph-path {x = x} {y} p q i .Edge = q i
  Graph-path {x = x} {y} p q i .Node-set = is-prop→pathp
     i  is-hlevel-is-prop {A = p i} 2) (x .Node-set) (y .Node-set) i
  Graph-path {x = x} {y} p q i .Edge-set {s} {t} =
    is-prop→pathp
       i  Π-is-hlevel 1 λ x  Π-is-hlevel 1 λ y  is-hlevel-is-prop {A = q i x y} 2)
       a b  x .Edge-set {a} {b})  a b  y .Edge-set {a} {b}) i s t

  graph-path :  {x y : Graph o } (h : x Graphs.≅ y)  x  y
  graph-path {x = x} {y = y} h = Graph-path (ua v)  i  E i ) module graph-path where
    module h = Graphs._≅_ h
    v :  x    y 
    v = record
      { fst = h.to .node
      ; snd = is-iso→is-equiv (iso (h.from .node) (happly (ap node h.invl)) (happly (ap node h.invr)))
      }

    E : (i : I)  ua v i  ua v i  Type 
    E i s t = Glue (y .Edge (unglue s) (unglue t))  where
      (i = i0)  x .Edge s t , _ , graph-iso-is-ff h.to (Graphs.iso→invertible h)
      (i = i1)  y .Edge s t , _ , id-equiv)

In particular, is a univalent category.

  Graphs-is-category : is-category (Graphs o )
  Graphs-is-category .to-path = graph-path
  Graphs-is-category .to-path-over {a} {b} p = Graphs.≅-pathp _ _ $ Graph-hom-pathp pv pe where
    open graph-path p

    pv : (h : I  a .Node)  PathP  i  ua v i) (h i0) (h.to .node (h i1))
    pv h i = ua-glue v i  { (i = i0)  h i }) (inS (h.to .node (h i)))

    pe : {x y : I  a .Node} (e :  i  a .Edge (x i) (y i))
        PathP  i  graph-path p i .Edge (pv x i) (pv y i)) (e i0) (h.to .edge (e i1))
    pe {x} {y} e i = attach ( i)  { (i = i0)  _ ; (i = i1)  _ }) (inS (h.to .edge (e i)))

Graphs as presheaves🔗

A graph may equivalently be seen as a diagram

of sets.

That is, a graph 2 is the same as functor from the walking parallel arrows category to Furthermore, presheaves and functors to are equivalent as this category is self-dual.

  graph→presheaf : Functor (Graphs o ) (PSh (o  ) ·⇇·)
  graph→presheaf .F₀ G =
    let
      it = Fork {a = el! $ Σ[ s  G ] Σ[ t  G ] G .Edge s t }
        {el! $ Lift   G }
        (lift  fst) (lift  fst  snd)
    in opFˡ (opFˡ it)

  graph→presheaf .F₁ f .η true  a = lift (f .node (a .lower))
  graph→presheaf .F₁ f .η false a = _ , _ , f .edge (a .snd .snd)
  graph→presheaf .F₁ f .is-natural x y idh = refl
  graph→presheaf .F₁ f .is-natural x y inl = refl
  graph→presheaf .F₁ f .is-natural x y inr = refl

  graph→presheaf .F-id = ext λ where
    true  x  refl
    false x  refl
  graph→presheaf .F-∘ G H = ext λ where
    true  x  refl
    false x  refl

  g→p-is-ff : is-fully-faithful graph→presheaf
  g→p-is-ff {x = x} {y = y} = is-iso→is-equiv (iso from ir il) where
    from : graph→presheaf · x => graph→presheaf · y  Graph-hom x y
    from h .node v = h .η true (lift v) .lower
    from h .edge e =
      let
        (s' , t' , e') = h .η false (_ , _ , e)
        ps = ap lower (sym (h .is-natural _ _ inl $ₚ (_ , _ , e)))
        pt = ap lower (sym (h .is-natural _ _ inr $ₚ (_ , _ , e)))
      in subst₂ (y .Edge) ps pt e'

    ir : is-right-inverse from (graph→presheaf .F₁)
    ir h = ext λ where
      true x           refl
      false (s , t , e) 
        let
          ps = ap lower (h .is-natural _ _ inl $ₚ (s , t , e))
          pt = ap lower (h .is-natural _ _ inr $ₚ (s , t , e))
          s' , t' , e' = h .η false (_ , _ , e)
        in Σ-pathp ps (Σ-pathp pt λ i  coe1→i  j  y .Edge (ps j) (pt j)) i e')

    il : is-left-inverse from (graph→presheaf .F₁)
    il h = Graph-hom-path  _  refl)  e  transport-refl _)

private module _ { : Level} where
  presheaf→graph :  PSh  ·⇇·   Graph  
  presheaf→graph F = g where
    module F = Functor F

    g : Graph  
    g .Node =  F · true 
    g .Edge s d = Σ[ e   F.₀ false  ]  F.₁ inl e  s × F.₁ inr e  d
    g .Node-set = hlevel 2
    g .Edge-set = hlevel 2

  open is-precat-iso
  open is-iso
  g→p-is-iso : is-precat-iso (graph→presheaf {} {})
  g→p-is-iso .has-is-ff = g→p-is-ff
  g→p-is-iso .has-is-iso = is-iso→is-equiv F₀-iso where
    F₀-iso : is-iso (graph→presheaf .F₀)
    F₀-iso .from = presheaf→graph
    F₀-iso .rinv F = Functor-path
       { false   n-ua (Iso→Equiv (
             (_ , _ , x , _ , _)  x) , iso
             s  _ , _ , s , refl , refl)
             _  refl)
             (_ , _ , s , p , q) i  p i , q i , s
                                     ,  j  p (i  j)) ,  j  q (i  j)))))
          ; true  n-ua (lower , is-iso→is-equiv (iso lift  _  refl)  _  refl)))
          })
      λ { {false} {false} idh  ua→ λ _  path→ua-pathp _ (sym (F .F-id {false} · _))
        ; {false} {true}  inl  ua→ λ (_ , _ , s , p , q)  path→ua-pathp _ (sym p)
        ; {false} {true}  inr  ua→ λ (_ , _ , s , p , q)  path→ua-pathp _ (sym q)
        ; {true}  {true}  idh  ua→ λ _  path→ua-pathp _ (sym (F .F-id {true} · _)) }
    F₀-iso .linv G = let
      eqv : Lift   G    G 
      eqv = Lift-≃

      ΣE = Σ[ s  G ] Σ[ t  G ] G .Edge s t

      E' : Lift   G   Lift   G   Type _
      E' x y = Σ[ (s , t , e)  ΣE ] (lift s  x × lift t  y)

      from : (u v :  G )  E' (lift u) (lift v)  G .Edge u v
      from u v ((u' , v' , e) , p , q) = subst₂ (G .Edge) (ap lower p) (ap lower q) e

      from-is : (u v :  G )  is-iso (from u v)
      from-is u v = iso  e  ((_ , _ , e) , refl , refl))  x  transport-refl _)
         ((u' , v' , e) , p , q) i 
          ( p (~ i) .lower , q (~ i) .lower
          , coe0→i  i  G .Edge (p i .lower) (q i .lower)) (~ i) e )
          ,  j  p (~ i  j))
          ,  j  q (~ i  j)))
      in Graph-path (ua eqv) λ i x y  Glue (G .Edge (ua-unglue eqv i x)
                                                     (ua-unglue eqv i y)) λ where
        (i = i0)  E' x y , from (x .lower) (y .lower) , is-iso→is-equiv (from-is _ _)
        (i = i1)  G .Edge x y , _ , id-equiv

Thus, are presheaves and are thereby a topos.

  graphs-are-presheaves : Equivalence (Graphs  ) (PSh  ·⇇·)
  graphs-are-presheaves = eqv where
    open Equivalence
    eqv : Equivalence (Graphs  ) (PSh  ·⇇·)
    eqv .To = graph→presheaf
    eqv .To-equiv = is-precat-iso→is-equivalence g→p-is-iso

The underlying graph of a strict category🔗

Note that every strict category has an underlying graph where the nodes are given by objects and edges by morphisms. Moreover, functors between strict categories give rise to graph homomorphisms between underlying graphs. This gives rise to a functor from the category of strict categories to the category of graphs.

Strict-cats↪Graphs : Functor (Strict-cats o ) (Graphs o )
Strict-cats↪Graphs .F₀ (C , C-strict) .Node = Precategory.Ob C
Strict-cats↪Graphs .F₀ (C , C-strict) .Edge = Precategory.Hom C
Strict-cats↪Graphs .F₀ (C , C-strict) .Node-set = C-strict
Strict-cats↪Graphs .F₀ (C , C-strict) .Edge-set = hlevel 2
Strict-cats↪Graphs .F₁ F .node = F .F₀
Strict-cats↪Graphs .F₁ F .edge = F .F₁
Strict-cats↪Graphs .F-id = Graph-hom-path  _  refl)  _  refl)
Strict-cats↪Graphs .F-∘ F G = Graph-hom-path  _  refl)  _  refl)

The underlying graph functor is faithful, as functors are graph homomorphisms with extra properties.

Strict-cats↪Graphs-faithful : is-faithful (Strict-cats↪Graphs {o} {})
Strict-cats↪Graphs-faithful p =
  Functor-path
     x i  p i .node x)
     e i  p i .edge e)

  1. and, even more pedantically, a directed multi-↩︎

  2. whose edges and nodes live in the same universe↩︎