Show that graphs are presheaves (the1lab#471)

Co-authored-by: Amélia <[email protected]>
Co-authored-by: Naïm Camille Favier <[email protected]>

Author: 3 people

src/Cat/Instances/Graphs.lagda.md

@@ -7,9 +7,13 @@ description: |
 open import 1Lab.Path.Cartesian
 open import 1Lab.Reflection
 
+open import Cat.Functor.Equivalence.Path
+open import Cat.Instances.Shape.Parallel
+open import Cat.Functor.Equivalence
 open import Cat.Instances.StrictCat
 open import Cat.Functor.Properties
 open import Cat.Functor.Base
+open import Cat.Univalent
 open import Cat.Prelude
 open import Cat.Strict
 
@@ -145,6 +149,11 @@ Graph-hom-path {G = G} {H = H} p0 p1 =
 instance
   Funlike-Graph-hom : Funlike (Graph-hom G H) ⌞ G ⌟ λ _ → ⌞ H ⌟
   Funlike-Graph-hom .Funlike._#_ = vertex
+
+Graph-hom-id : {G : Graph o ℓ} → Graph-hom G G
+Graph-hom-id .vertex v = v
+Graph-hom-id .edge e = e
+
 ```
 -->
 
@@ -155,30 +164,221 @@ 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 .vertex v = v
-Graphs o ℓ .Precategory.id .edge e = e
+Graphs o ℓ .Precategory.id = Graph-hom-id
 Graphs o ℓ .Precategory._∘_ f g .vertex v = f .vertex (g .vertex v)
 Graphs o ℓ .Precategory._∘_ f g .edge e = f .edge (g .edge e)
 Graphs o ℓ .Precategory.idr _ = Graph-hom-path (λ _ → refl) (λ _ → refl)
 Graphs o ℓ .Precategory.idl _ = Graph-hom-path (λ _ → refl) (λ _ → refl)
 Graphs o ℓ .Precategory.assoc _ _ _ = Graph-hom-path (λ _ → refl) (λ _ → refl)
+```
+<!--
+```agda
+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 vertex h.invr # _) (ap vertex h.invr # _) (h.inv .edge e)
+
+    ir : is-right-inverse from (h .edge)
+    ir e =
+      let
+        lemma = J₂
+          (λ s'' t'' p q → ∀ e
+            → h .edge (subst₂ (x .Edge) p q e)
+            ≡ subst₂ (y .Edge) (ap# h p) (ap# h q) (h .edge e))
+          (λ e → ap (h .edge) (transport-refl _) ∙ sym (transport-refl _))
+      in lemma _ _ (h.inv .edge e)
+      ·· ap₂ (λ p q → subst₂ (y .Edge) {b' = h .vertex t} p q (h .edge (h.inv .edge e))) prop! prop!
+      ·· from-pathp (λ i → h.invl i .edge 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 .Vertex ≡ y .Vertex)
+    → (PathP (λ i → p i → p i → Type ℓ) (x .Edge) (y .Edge))
+    → x ≡ y
+  Graph-path {x = x} {y} p q i .Vertex = p i
+  Graph-path {x = x} {y} p q i .Edge = q i
+  Graph-path {x = x} {y} p q i .Vertex-is-set = is-prop→pathp
+    (λ i → is-hlevel-is-prop {A = p i} 2) (x .Vertex-is-set) (y .Vertex-is-set) i
+  Graph-path {x = x} {y} p q i .Edge-is-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-is-set {a} {b}) (λ a b → y .Edge-is-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 .vertex
+      ; snd = is-iso→is-equiv (iso (h.from .vertex) (happly (ap vertex h.invl)) (happly (ap vertex 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, $\Graphs$ is a [[univalent category]].
+
+```agda
+  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 .Vertex) → PathP (λ i → ua v i) (h i0) (h.to .vertex (h i1))
+    pv h i = ua-glue v i (λ { (i = i0) → h i }) (inS (h.to .vertex (h i)))
 
-module Graphs {o} {ℓ} = Cat.Reasoning (Graphs o ℓ)
+    pe : {x y : I → a .Vertex} (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 $(V, E)$ may equivalently be seen as a diagram
+
+~~~{.quiver}
+\begin{tikzcd}
+	V & E & V
+	\arrow["{\mathrm{src}}"', from=1-2, to=1-1]
+	\arrow["{\mathrm{dst}}", from=1-2, to=1-3]
+\end{tikzcd}
+~~~
+
+of sets.
+
+That is, a graph $G$^[whose edges and vertices live in the same
+universe] is the same as functor from the [[walking parallel arrows]]
+category to $\Sets$. Furthermore, presheaves and functors to $\Sets$ are
+equivalent as this category is self-dual.
+
 <!--
 ```agda
-open Functor
+  graph→presheaf : Functor (Graphs o ℓ) (PSh (o ⊔ ℓ) ·⇇·)
+  graph→presheaf .F₀ G =
+    Fork {a = el! $ Σ[ s ∈ G .Vertex ] Σ[ t ∈ G .Vertex ] G .Edge s t }
+         {el! $ Lift ℓ ⌞ G ⌟}
+         (lift ⊙ fst)
+         (lift ⊙ fst ⊙ snd)
+  graph→presheaf .F₁ f =
+    Fork-nt {u = λ (s , t , e) → f .vertex s , f .vertex t , f .edge e }
+            {v = λ { (lift v) → lift (f # v) } } refl refl
+  graph→presheaf .F-id = Nat-path λ { true → refl ; false → refl }
+  graph→presheaf .F-∘ G H = Nat-path λ { true → refl ; false → 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 .vertex v = h .η true (lift v) .lower
+    from h .edge e =
+      let
+        (s' , t' , e') = h .η false (_ , _ , e)
+        ps = ap lower (sym (h .is-natural false true false $ₚ (_ , _ , e)))
+        pt = ap lower (sym (h .is-natural false true true $ₚ (_ , _ , 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 false true false $ₚ (s , t , e))
+          pt = ap lower (h .is-natural false true true $ₚ (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 .Vertex = ⌞ F # true ⌟
+          g .Edge s d = Σ[ e ∈ ∣ F.₀ false ∣ ]  F.₁ false e ≡ s × F.₁ true e ≡ d
+          g .Vertex-is-set = hlevel 2
+          g .Edge-is-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 .inv = 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} e → ua→ λ _ → path→ua-pathp _ (sym (F .F-id {false} # _))
+        ; {false} {true} false → ua→ λ (_ , _ , s , p , q) → path→ua-pathp _ (sym p)
+        ; {false} {true} true → ua→ λ (_ , _ , s , p , q) → path→ua-pathp _ (sym q)
+        ; {true} {true} e → 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
+
+      frome : (u v : ⌞ G ⌟) → is-iso (from u v)
+      frome 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 (frome _ _)
+        (i = i1) → G .Edge x y , _ , id-equiv
 ```
 -->
 
-:::{.definition #underlying-graph alias="underlying-graph-functor"}
+Thus, $\Graphs$ are presheaves and are thereby a [[topos]].
+
+```agda
+  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 {defines="underlying-graph underlying-graph-functor"}
+
 Note that every [[strict category]] has an underlying graph, where
 the vertices 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.
-:::
 
 ```agda
 Strict-cats↪Graphs : Functor (Strict-cats o ℓ) (Graphs o ℓ)

src/Cat/Instances/Shape/Parallel.lagda.md

@@ -24,7 +24,7 @@ open is-iso
 ```
 -->
 
-# The "parallel arrows" category {defines="parallel-arrows"}
+# The "parallel arrows" category {defines="parallel-arrows walking-parallel-arrows"}
 
 The parallel arrows category is the category with two objects, and two
 parallel arrows between them. It is the shape of [[equaliser]] and

src/Topoi/Base.lagda.md

@@ -45,7 +45,7 @@ open _=>_
 ```
 -->
 
-# Grothendieck topoi
+# Grothendieck topoi {defines="topos topoi"}
 
 Topoi are an abstraction introduced by Alexander Grothendieck in the
 1960s as a generalisation of [topological spaces], suitable for his work