Redefine (co)limits in terms of kan extensions (#186)

# Description This PR refactors (co)limits to be defined in terms of kan extensions. The main motivation for doing so is to make preservation of limits less annoying to deal with; as it currently stands we need to define special functions for mapping cones, which makes life much harder. ## Notes As noted on discord, representability does not work due to (annoying!) universe level issues. This PR is also based off #184; I'll rebase when the time comes. --------- Co-authored-by: Amélia Liao <[email protected]>
the1lab · Mar 21, 2023 · f6b6f0d · f6b6f0d
1 parent 26bdece
commit f6b6f0d
Show file tree

Hide file tree

Showing 120 changed files with 6,620 additions and 3,267 deletions.
diff --git a/src/1Lab/Path.lagda.md b/src/1Lab/Path.lagda.md
@@ -1200,6 +1200,18 @@ ap₂ : ∀ {a b c} {A : Type a} {B : A → Type b} {C : (x : A) → B x → Typ
 ap₂ f p q i = f (p i) (q i)
 ```
 
+<!--
+```agda
+apd : ∀ {a b} {A : I → Type a} {B : (i : I) → A i → Type b}
+    → (f : (i : I) → (a : A i) → B i a)
+    → {x : A i0}
+    → {y : A i1}
+    → (p : PathP A x y)
+    → PathP (λ i → B i (p i)) (f i0 x) (f i1 y)
+apd f p i = f i (p i)
+```
+-->
+
 This operation satisfies many identities definitionally that are only
 propositional when `ap`{.Agda} is defined in terms of `J`{.Agda}. For
 instance:

diff --git a/src/Algebra/Group/Cat/FinitelyComplete.lagda.md b/src/Algebra/Group/Cat/FinitelyComplete.lagda.md
@@ -234,14 +234,14 @@ $g$.
   Groups-equalisers .apex = Equaliser-group
   Groups-equalisers .equ = total-hom fst record { pres-⋆ = λ x y → refl }
   Groups-equalisers .has-is-eq .equal = Forget-is-faithful seq.equal
-  Groups-equalisers .has-is-eq .limiting {F = F} {e′} p = total-hom map lim-gh where
-    map = seq.limiting {F = underlying-set (F .snd)} (ap hom p)
+  Groups-equalisers .has-is-eq .universal {F = F} {e′} p = total-hom map lim-gh where
+    map = seq.universal {F = underlying-set (F .snd)} (ap hom p)
 
     lim-gh : is-group-hom _ _ map
     lim-gh .pres-⋆ x y = Σ-prop-path (λ _ → H.has-is-set _ _) (e′ .preserves .pres-⋆ _ _)
 
-  Groups-equalisers .has-is-eq .universal {F = F} {p = p} = Forget-is-faithful
-    (seq.universal {F = underlying-set (F .snd)} {p = ap hom p})
+  Groups-equalisers .has-is-eq .factors {F = F} {p = p} = Forget-is-faithful
+    (seq.factors {F = underlying-set (F .snd)} {p = ap hom p})
 
   Groups-equalisers .has-is-eq .unique {F = F} {p = p} q = Forget-is-faithful
     (seq.unique {F = underlying-set (F .snd)} {p = ap hom p} (ap hom q))

diff --git a/src/Algebra/Group/Subgroup.lagda.md b/src/Algebra/Group/Subgroup.lagda.md
@@ -319,7 +319,7 @@ will compute.
       path : (x : ⌞ Kerf.ker ⌟) → A→im # A.unit ≡ A→im # (x .fst)
       path (x* , p) = Tpath (f.pres-id ∙ sym p)
 
-    coeq .coequalise {F = F} {e′ = e'} p = gh where
+    coeq .universal {F = F} {e′ = e'} p = gh where
       module F = Group-on (F .snd)
       module e' = is-group-hom (e' .preserves)
 
@@ -330,7 +330,7 @@ will compute.
           {P = λ q r → elim p (((x , q) Ak.⋆ (y , r)) .snd) ≡ elim p q F.⋆ elim p r}
           (λ _ _ → F.has-is-set _ _) (λ x y → e'.pres-⋆ _ _) q r
 
-    coeq .universal = Forget-is-faithful refl
+    coeq .factors = Forget-is-faithful refl
 
     coeq .unique {F} {p = p} {colim = colim} prf = Forget-is-faithful (funext path)
       where abstract
@@ -341,7 +341,7 @@ will compute.
             {P = λ q → colim # (x , q) ≡ elim p q}
             (λ _ → F.has-is-set _ _)
             (λ { (f , fp) → ap (colim #_) (Σ-prop-path (λ _ → squash) (sym fp))
-                          ∙ sym (happly (ap hom prf) f) })
+                          ∙ (happly (ap hom prf) f) })
             t
 ```
 

diff --git a/src/Algebra/Ring/Module.lagda.md b/src/Algebra/Ring/Module.lagda.md
@@ -12,8 +12,8 @@ open import Cat.Displayed.Fibre
 open import Cat.Displayed.Total
 open import Cat.Functor.Adjoint
 open import Cat.Displayed.Base
-open import Cat.Abelian.Endo
 open import Cat.Abelian.Base
+open import Cat.Abelian.Endo
 open import Cat.Prelude
 
 import Cat.Reasoning

diff --git a/src/Cat/Abelian/Base.lagda.md b/src/Cat/Abelian/Base.lagda.md
@@ -316,7 +316,7 @@ monomorphism].
   decompose {A} {B} f = map , sym path
     where
       proj′ : Hom (Coker.coapex (Ker.kernel f)) B
-      proj′ = Coker.coequalise (Ker.kernel f) {e′ = f} $ sym path
+      proj′ = Coker.universal (Ker.kernel f) {e′ = f} $ sym path
 ```
 
 <!--
@@ -332,7 +332,7 @@ monomorphism].
 
 ```agda
       map : Hom (Coker.coapex (Ker.kernel f)) (Ker.ker (Coker.coeq f))
-      map = Ker.limiting (Coker.coeq f) {e′ = proj′} $ sym path
+      map = Ker.universal (Coker.coeq f) {e′ = proj′} $ sym path
 ```
 
 The existence of the map $f'$, and indeed of the maps $p$ and $i$,
@@ -345,16 +345,16 @@ the canonical subobject inclusion $\ker(f) \to B$.
         where abstract
           path : ∅.zero→ ∘ proj′ ≡ Coker.coeq f ∘ proj′
           path = Coker.unique₂ (Ker.kernel f)
-            {e′ = 0m} {p = ∘-zero-r ∙ sym ∘-zero-l}
-            (sym ( pushl (∅.zero-∘r _) ∙ pulll ( ap₂ _∘_ refl (∅.has⊤ _ .paths 0m)
+            {e′ = 0m} (∘-zero-r ∙ sym ∘-zero-l)
+            (pushl (∅.zero-∘r _) ∙ pulll ( ap₂ _∘_ refl (∅.has⊤ _ .paths 0m)
                                                ∙ ∘-zero-r)
-                 ∙ ∘-zero-l))
-            (sym ( pullr (Coker.universal (Ker.kernel f)) ∙ sym (Coker.coequal _)
-                 ∙ ∘-zero-r))
+                 ∙ ∘-zero-l)
+            (pullr (Coker.factors (Ker.kernel f)) ∙ sym (Coker.coequal _)
+                 ∙ ∘-zero-r)
 
       path =
-        Ker.kernel (Coker.coeq f) ∘ map ∘ Coker.coeq (Ker.kernel f) ≡⟨ pulll (Ker.universal _) ⟩
-        proj′ ∘ Coker.coeq (Ker.kernel f)                           ≡⟨ Coker.universal _ ⟩
+        Ker.kernel (Coker.coeq f) ∘ map ∘ Coker.coeq (Ker.kernel f) ≡⟨ pulll (Ker.factors _) ⟩
+        proj′ ∘ Coker.coeq (Ker.kernel f)                           ≡⟨ Coker.factors _ ⟩
         f                                                           ∎
 ```
 -->
@@ -410,7 +410,7 @@ $f$ is mono), we have $0 = \ker f$ from $f0 = f\ker f$.
 ```agda
       kercoker→f : m.Hom (cut (Ker.kernel (Coker.coeq f))) (cut f)
       kercoker→f ./-Hom.map =
-        Coker.coequalise (Ker.kernel f) {e′ = id} (monic _ _ path) ∘
+        Coker.universal (Ker.kernel f) {e′ = id} (monic _ _ path) ∘
           coker-ker≃ker-coker f .is-invertible.inv
         where abstract
           path : f ∘ id ∘ 0m ≡ f ∘ id ∘ Ker.kernel f
@@ -429,15 +429,15 @@ coequalisers are epic to make progress.
       kercoker→f ./-Hom.commutes = path where
         lemma =
           is-coequaliser→is-epic (Coker.coeq _) (Coker.has-is-coeq _) _ _ $
-               pullr (Coker.universal _)
+               pullr (Coker.factors _)
             ·· elimr refl
             ·· (decompose f .snd ∙ assoc _ _ _)
 
         path =
           invertible→epic (coker-ker≃ker-coker _) _ _ $
-            (f ∘ Coker.coequalise _ _ ∘ _) ∘ decompose f .fst   ≡⟨ ap₂ _∘_ (assoc _ _ _) refl ⟩
-            ((f ∘ Coker.coequalise _ _) ∘ _) ∘ decompose f .fst ≡⟨ cancelr (coker-ker≃ker-coker _ .is-invertible.invr) ⟩
-            f ∘ Coker.coequalise _ _                            ≡⟨ lemma ⟩
+            (f ∘ Coker.universal _ _ ∘ _) ∘ decompose f .fst   ≡⟨ ap₂ _∘_ (assoc _ _ _) refl ⟩
+            ((f ∘ Coker.universal _ _) ∘ _) ∘ decompose f .fst ≡⟨ cancelr (coker-ker≃ker-coker _ .is-invertible.invr) ⟩
+            f ∘ Coker.universal _ _                            ≡⟨ lemma ⟩
             Ker.kernel _ ∘ decompose f .fst                     ∎
 ```
 
@@ -450,19 +450,19 @@ $\cA$, thus assemble into an isomorphism in the slice.
     mono→kernel = m.make-iso f→kercoker kercoker→f f→kc→f kc→f→kc where
       f→kc→f : f→kercoker m.∘ kercoker→f ≡ m.id
       f→kc→f = /-Hom-path $
-        (decompose f .fst ∘ Coker.coeq _) ∘ Coker.coequalise _ _ ∘ _ ≡⟨ cancel-inner lemma ⟩
+        (decompose f .fst ∘ Coker.coeq _) ∘ Coker.universal _ _ ∘ _  ≡⟨ cancel-inner lemma ⟩
         decompose f .fst ∘ _                                         ≡⟨ coker-ker≃ker-coker f .is-invertible.invl ⟩
         id                                                           ∎
         where
           lemma = Coker.unique₂ _
             {e′ = Coker.coeq (Ker.kernel f)}
-            {p = ∘-zero-r ∙ sym (sym (Coker.coequal _) ∙ ∘-zero-r)}
-            (sym (pullr (Coker.universal (Ker.kernel f)) ∙ elimr refl))
-            (introl refl)
+            (∘-zero-r ∙ sym (sym (Coker.coequal _) ∙ ∘-zero-r))
+            (pullr (Coker.factors (Ker.kernel f)) ∙ elimr refl)
+            (eliml refl)
 
       kc→f→kc : kercoker→f m.∘ f→kercoker ≡ m.id
       kc→f→kc = /-Hom-path $
-        (Coker.coequalise _ _ ∘ _) ∘ decompose f .fst ∘ Coker.coeq _ ≡⟨ cancel-inner (coker-ker≃ker-coker f .is-invertible.invr) ⟩
-        Coker.coequalise _ _ ∘ Coker.coeq _                          ≡⟨ Coker.universal _ ⟩
+        (Coker.universal _ _ ∘ _) ∘ decompose f .fst ∘ Coker.coeq _ ≡⟨ cancel-inner (coker-ker≃ker-coker f .is-invertible.invr) ⟩
+        Coker.universal _ _ ∘ Coker.coeq _                          ≡⟨ Coker.factors _ ⟩
         id                                                           ∎
 ```
diff --git a/src/Cat/Abelian/Images.lagda.md b/src/Cat/Abelian/Images.lagda.md
@@ -81,7 +81,7 @@ $$
 
 ```agda
   the-img .map ./-Hom.map = decompose f .fst ∘ Coker.coeq _
-  the-img .map ./-Hom.commutes = pulll (Ker.universal _) ∙ Coker.universal _
+  the-img .map ./-Hom.commutes = pulll (Ker.factors _) ∙ Coker.factors _
 ```
 
 ## Universality
@@ -115,7 +115,7 @@ commutes.
     factor : ↓Hom (const! (cut f)) Forget-full-subcat the-img other
     factor .α = tt
     factor .β ./-Hom.map =
-        Coker.coequalise (Ker.kernel f) {e′ = other .map .map} path
+        Coker.universal (Ker.kernel f) {e′ = other .map .map} path
       ∘ coker-ker≃ker-coker f .is-invertible.inv
 ```
 
@@ -144,19 +144,21 @@ is the image of $f$.
 
 <details>
 <summary>Here's the tedious isomorphism algebra.</summary>
+
 ```agda
     factor .β ./-Hom.commutes = invertible→epic (coker-ker≃ker-coker f) _ _ $
-      Coker.unique₂ (Ker.kernel f) {e′ = f}
-        {p = sym (Ker.equal f ∙ ∅.zero-∘r _ ∙ 0m-unique ∙ sym ∘-zero-r)}
-        (sym ( ap₂ _∘_ ( sym (assoc _ _ _)
+      Coker.unique₂ (Ker.kernel f)
+        (sym (Ker.equal f ∙ ∅.zero-∘r _ ∙ 0m-unique ∙ sym ∘-zero-r))
+        (ap₂ _∘_ ( sym (assoc _ _ _)
                         ∙ ap₂ _∘_ refl (cancelr
                           (coker-ker≃ker-coker f .is-invertible.invr))) refl
-              ∙ pullr (Coker.universal _) ∙ other .map .commutes))
-        (decompose f .snd ∙ assoc _ _ _)
+              ∙ pullr (Coker.factors _) ∙ other .map .commutes)
+        (sym (decompose f .snd ∙ assoc _ _ _))
     factor .sq = /-Hom-path $ sym $ other .y .witness _ _ $
-          pulll (factor .β .commutes)
-      ·· the-img .map .commutes
-      ·· (sym (other .map .commutes) ∙ ap (other .y .object .map ∘_) (intror refl))
+      pulll (factor .β .commutes)
+      ∙ the-img .map .commutes
+      ·· sym (other .map .commutes)
+      ·· ap (other .y .object .map ∘_) (intror refl)
 
     unique : ∀ x → factor ≡ x
     unique x = ↓Hom-path _ _ refl $ /-Hom-path $ other .y .witness _ _ $

diff --git a/src/Cat/Abelian/Limits.lagda.md b/src/Cat/Abelian/Limits.lagda.md
@@ -61,13 +61,13 @@ module _ (A : is-pre-abelian C) where
       (f - g) ∘ Ker.kernel (f - g)                        ≡⟨ Ker.equal (f - g) ⟩
       ∅.zero→ ∘ Ker.kernel (f - g)                        ≡⟨ ∅.zero-∘r _ ∙ 0m-unique ⟩
       0m                                                  ∎
-    equ .limiting {e′ = e′} p = Ker.limiting (f - g) {e′ = e′} $
+    equ .universal {e′ = e′} p = Ker.universal (f - g) {e′ = e′} $
       (f - g) ∘ e′         ≡˘⟨ ∘-minus-l _ _ _ ⟩
       f ∘ e′ - g ∘ e′      ≡⟨ ap (f ∘ e′ -_) (sym p) ⟩
       f ∘ e′ - f ∘ e′      ≡⟨ Hom.inverser ⟩
       0m                   ≡˘⟨ ∅.zero-∘r _ ∙ 0m-unique ⟩
       Zero.zero→ ∅ ∘ e′    ∎
-    equ .universal = Ker.universal _
+    equ .factors = Ker.factors _
     equ .unique = Ker.unique (f - g)
 ```
 

diff --git a/src/Cat/Base.lagda.md b/src/Cat/Base.lagda.md
@@ -473,6 +473,12 @@ module _ where
   Const {D = D} x .F-id = refl
   Const {D = D} x .F-∘ _ _ = sym (idr D _)
 
+  const-nt : ∀ {o ℓ o′ ℓ′} {C : Precategory o ℓ} {D : Precategory o′ ℓ′}
+           → {x y : Ob D} → Hom D x y
+           → Const {C = C} {D = D} x => Const {C = C} {D = D} y
+  const-nt f ._=>_.η _ = f
+  const-nt {D = D} f ._=>_.is-natural _ _ _ = idr D _ ∙ sym (idl D _)
+
 infixr 30 _F∘_
 infix 20 _=>_
 
@@ -486,6 +492,7 @@ module _ {o₁ h₁ o₂ h₂}
     module D = Precategory D
     module C = Precategory C
 
+  open Functor
   open _=>_
 ```
 -->
@@ -531,5 +538,11 @@ is a proposition:
   _ηₚ_ : ∀ {a b : F => G} → a ≡ b → ∀ x → a .η x ≡ b .η x
   p ηₚ x = ap (λ e → e .η x) p
 
+  _ηᵈ_ : ∀ {F' G' : Functor C D} {p : F ≡ F'} {q : G ≡ G'}
+       → {a : F => G} {b : F' => G'}
+       → PathP (λ i → p i => q i) a b
+       → ∀ x → PathP (λ i → D.Hom (p i .F₀ x) (q i .F₀ x)) (a .η x) (b .η x)
+  p ηᵈ x = apd (λ i e → e .η x) p
+
   infixl 45 _ηₚ_
 ```
diff --git a/src/Cat/Bi/Base.lagda.md b/src/Cat/Bi/Base.lagda.md
@@ -1,5 +1,5 @@
 ```agda
-open import Cat.Instances.Functor.Compose
+open import Cat.Instances.Functor.Compose renaming (_◆_ to _◇_)
 open import Cat.Instances.Functor
 open import Cat.Instances.Product
 open import Cat.Functor.Hom