Low hanging fruit regarding limits

src/Cat/Diagram/Coequaliser/RegularEpi.lagda.md

@@ -45,7 +45,7 @@ arrows $R \tto a$.
       {r}           : Ob
       {arr₁} {arr₂} : Hom r a
       has-is-coeq   : is-coequaliser C arr₁ arr₂ f
-  
+
     open is-coequaliser has-is-coeq public
 ```
 
@@ -55,7 +55,7 @@ fact epic:
 ```agda
     is-regular-epi→is-epic : is-epic f
     is-regular-epi→is-epic = is-coequaliser→is-epic _ has-is-coeq
-  
+
   open is-regular-epi using (is-regular-epi→is-epic) public
 ```
 
@@ -73,9 +73,9 @@ epis:
     field
       {kernel}       : Ob
       p₁ p₂          : Hom kernel a
-      is-kernel-pair : is-pullback C p₁ f p₂ f
+      has-kernel-pair : is-kernel-pair C p₁ p₂ f
       has-is-coeq    : is-coequaliser C p₁ p₂ f
-  
+
     is-effective-epi→is-regular-epi : is-regular-epi f
     is-effective-epi→is-regular-epi = re where
       open is-regular-epi hiding (has-is-coeq)
@@ -107,14 +107,14 @@ module _ {o ℓ} {C : Precategory o ℓ} where
   is-regular-epi→is-effective-epi {f = f} kp reg = epi where
     module reg = is-regular-epi reg
     module kp = Pullback kp
-  
+
     open is-effective-epi
     open is-coequaliser
     epi : is-effective-epi C f
     epi .kernel = kp.apex
     epi .p₁ = kp.p₁
     epi .p₂ = kp.p₂
-    epi .is-kernel-pair = kp.has-is-pb
+    epi .has-kernel-pair = kp.has-is-pb
     epi .has-is-coeq .coequal = kp.square
     epi .has-is-coeq .universal {F = F} {e'} p = reg.universal q where
       q : e' ∘ reg.arr₁ ≡ e' ∘ reg.arr₂

src/Cat/Diagram/Congruence.lagda.md

@@ -427,10 +427,10 @@ identifies _exactly those_ objects related by $R$, and no more.
 record is-effective-congruence {A} (R : Congruence-on A) : Type (o ⊔ ℓ) where
   private module R = Congruence-on R
   field
-    {A/R}          : Ob
-    quotient       : Hom A A/R
-    has-quotient   : is-quotient-of R quotient
-    is-kernel-pair : is-pullback C R.rel₁ quotient R.rel₂ quotient
+    {A/R}           : Ob
+    quotient        : Hom A A/R
+    has-quotient    : is-quotient-of R quotient
+    has-kernel-pair : is-kernel-pair C R.rel₁ R.rel₂ quotient
 ```
 
 If $f$ is the coequaliser of its kernel pair --- that is, it is an
@@ -454,7 +454,7 @@ kernel-pair-is-effective {a = a} {b} {f} quot = epi where
   epi .is-effective-congruence.A/R = b
   epi .quotient = f
   epi .has-quotient = quot
-  epi .is-kernel-pair =
+  epi .has-kernel-pair =
     transport
       (λ i → is-pullback C (a×a.π₁∘factor {p1 = pb.p₁} {p2 = pb.p₂} (~ i)) f
                            (a×a.π₂∘factor {p1 = pb.p₁} {p2 = pb.p₂} (~ i)) f)
@@ -471,6 +471,6 @@ kp-effective-congruence→effective-epi {f = f} cong = epi where
   epi .kernel = Kernel-pair _ .Congruence-on.domain
   epi .p₁ = _
   epi .p₂ = _
-  epi .is-kernel-pair = cong.is-kernel-pair
+  epi .has-kernel-pair = cong.has-kernel-pair
   epi .has-is-coeq = cong.has-quotient
 ```

src/Cat/Diagram/Coproduct/Indexed.lagda.md

@@ -98,9 +98,131 @@ Lift-Indexed-coproduct
   → Indexed-coproduct {Idx = Lift ℓ' I} (F ⊙ Lift.lower)
   → Indexed-coproduct F
 Lift-Indexed-coproduct _ = Indexed-coproduct-≃ (Lift-≃ e⁻¹)
+
+is-indexed-coproduct-is-prop
+  : ∀ {ℓ'} {Idx : Type ℓ'}
+  → {F : Idx → C.Ob} {ΣF : C.Ob} {ι : ∀ idx → C.Hom (F idx) ΣF}
+  → is-prop (is-indexed-coproduct F ι)
+is-indexed-coproduct-is-prop {Idx = Idx} {F} {ΣF} {ι} P Q = path where
+  open is-indexed-coproduct
+
+  p : ∀ {X} → (f : ∀ i → C.Hom (F i) X) → P .match f ≡ Q .match f
+  p f = Q .unique f (λ i → P .commute)
+
+  path : P ≡ Q
+  path i .match f = p f i
+  path i .commute {i = idx} {f = f} =
+    is-prop→pathp (λ i → C.Hom-set _ _ (p f i C.∘ ι idx) (f idx))
+      (P .commute)
+      (Q .commute) i
+  path i .unique {h = h} f q =
+    is-prop→pathp (λ i → C.Hom-set _ _ h (p f i))
+      (P .unique f q)
+      (Q .unique f q) i
+
+module _ {ℓ'} {Idx : Type ℓ'} {F : Idx → C.Ob} {P P' : Indexed-coproduct F} where
+  private
+    module P = Indexed-coproduct P
+    module P' = Indexed-coproduct P'
+
+  Indexed-coproduct-path
+    : (p : P.ΣF ≡ P'.ΣF)
+    → (∀ idx → PathP (λ i → C.Hom (F idx) (p i)) (P.ι idx) (P'.ι idx))
+    → P ≡ P'
+  Indexed-coproduct-path p q i .Indexed-coproduct.ΣF = p i
+  Indexed-coproduct-path p q i .Indexed-coproduct.ι idx = q idx i
+  Indexed-coproduct-path p q i .Indexed-coproduct.has-is-ic =
+    is-prop→pathp (λ i → is-indexed-coproduct-is-prop {ΣF = p i} {ι = λ idx → q idx i})
+      P.has-is-ic
+      P'.has-is-ic i
 ```
 -->
 
+## Uniqueness
+
+As universal constructions, indexed coproducts are unique up to isomorphism.
+The proof follows the usual pattern: we use the universal morphisms to
+construct morphisms in both directions, and uniqueness ensures that these
+maps form an isomorphism.
+
+```agda
+is-indexed-coproduct→iso
+  : ∀ {ℓ'} {Idx : Type ℓ'} {F : Idx → C.Ob}
+  → {ΣF ΣF' : C.Ob}
+  → {ι : ∀ i → C.Hom (F i) ΣF} {ι' : ∀ i → C.Hom (F i) ΣF'}
+  → is-indexed-coproduct F ι
+  → is-indexed-coproduct F ι'
+  → ΣF C.≅ ΣF'
+is-indexed-coproduct→iso {ι = ι} {ι' = ι'} ΣF-coprod ΣF'-coprod =
+  C.make-iso (ΣF.match ι') (ΣF'.match ι)
+    (ΣF'.unique₂ (λ i → C.pullr ΣF'.commute ∙ ΣF.commute ∙ sym (C.idl _)))
+    (ΣF.unique₂ (λ i → C.pullr ΣF.commute ∙ ΣF'.commute ∙ sym (C.idl _)))
+  where
+    module ΣF = is-indexed-coproduct ΣF-coprod
+    module ΣF' = is-indexed-coproduct ΣF'-coprod
+```
+
+<!--
+```agda
+Indexed-coproduct→iso
+  : ∀ {ℓ'} {Idx : Type ℓ'} {F : Idx → C.Ob}
+  → (P P' : Indexed-coproduct F)
+  → Indexed-coproduct.ΣF P C.≅ Indexed-coproduct.ΣF P'
+Indexed-coproduct→iso P P' =
+  is-indexed-coproduct→iso
+    (Indexed-coproduct.has-is-ic P)
+    (Indexed-coproduct.has-is-ic P')
+```
+-->
+
+## Properties
+
+Let $X : \Sigma A B \to \cC$ be a family of objects in $\cC$. If the
+the indexed coproducts $\Sigma_{a, b : \Sigma A B} X_{a,b}$ and
+$\Sigma_{a : A} \Sigma_{b : B(a)} X_{a, b}$ exists, then they are isomorphic.
+
+The formal statement of this is a bit of a mouthful, but all of these
+arguments are just required to ensure that the various coproducts actually
+exist.
+
+```agda
+is-indexed-coproduct-assoc
+  : ∀ {κ κ'} {A : Type κ} {B : A → Type κ'}
+  → {X : Σ A B → C.Ob}
+  → {ΣᵃᵇX : C.Ob} {ΣᵃΣᵇX : C.Ob} {ΣᵇX : A → C.Ob}
+  → {ιᵃᵇ : (ab : Σ A B) → C.Hom (X ab) ΣᵃᵇX}
+  → {ιᵃ : ∀ a → C.Hom (ΣᵇX a) ΣᵃΣᵇX}
+  → {ιᵇ : ∀ a → (b : B a) → C.Hom (X (a , b)) (ΣᵇX a)}
+  → is-indexed-coproduct X ιᵃᵇ
+  → is-indexed-coproduct ΣᵇX ιᵃ
+  → (∀ a → is-indexed-coproduct (λ b → X (a , b)) (ιᵇ a))
+  → ΣᵃᵇX C.≅ ΣᵃΣᵇX
+```
+
+Luckily, the proof of this fact is easier than the statement! Indexed
+coproducts are unique up to isomorphism, so it suffices to show that
+$\Sigma_{a : A} \Sigma_{b : B(a)} X_{a, b}$ is an indexed product
+over $X$, which follows almost immediately from our hypotheses.
+
+```agda
+is-indexed-coproduct-assoc {A = A} {B} {X} {ΣᵃΣᵇX = ΣᵃΣᵇX} {ιᵃ = ιᵃ} {ιᵇ} Σᵃᵇ ΣᵃΣᵇ Σᵇ =
+  is-indexed-coproduct→iso Σᵃᵇ Σᵃᵇ'
+  where
+    open is-indexed-coproduct
+
+    ιᵃᵇ' : ∀ (ab : Σ A B) → C.Hom (X ab) ΣᵃΣᵇX
+    ιᵃᵇ' (a , b) = ιᵃ a C.∘ ιᵇ a b
+
+    Σᵃᵇ' : is-indexed-coproduct X ιᵃᵇ'
+    Σᵃᵇ' .match f = ΣᵃΣᵇ .match λ a → Σᵇ a .match λ b → f (a , b)
+    Σᵃᵇ' .commute = C.pulll (ΣᵃΣᵇ .commute) ∙ Σᵇ _ .commute
+    Σᵃᵇ' .unique {h = h} f p =
+      ΣᵃΣᵇ .unique _ λ a →
+      Σᵇ _ .unique _ λ b →
+      sym (C.assoc _ _ _) ∙ p (a , b)
+```
+
+
 # Disjoint coproducts
 
 An indexed coproduct $\sum F$ is said to be **disjoint** if every one of

src/Cat/Diagram/Equaliser.lagda.md

@@ -39,12 +39,12 @@ right-hand-sides agree.
         : ∀ {F} {e' : Hom F A} {p : f ∘ e' ≡ g ∘ e'} {other : Hom F E}
         → equ ∘ other ≡ e'
         → other ≡ universal p
-  
+
     equal-∘ : f ∘ equ ∘ h ≡ g ∘ equ ∘ h
     equal-∘ {h = h} =
       f ∘ equ ∘ h ≡⟨ extendl equal ⟩
       g ∘ equ ∘ h ∎
-  
+
     unique₂
       : ∀ {F} {e' : Hom F A}  {o1 o2 : Hom F E}
       → f ∘ e' ≡ g ∘ e'
@@ -77,7 +77,7 @@ its domain:
       {apex}  : Ob
       equ     : Hom apex A
       has-is-eq : is-equaliser f g equ
-  
+
     open is-equaliser has-is-eq public
 ```
 
@@ -106,6 +106,70 @@ module _ {o ℓ} {C : Precategory o ℓ} where
     where open is-equaliser equalises
 ```
 
+## Uniqueness
+
+As universal constructions, equalisers are unique up to isomorphism.
+The proof follows the usual pattern: if $E, E'$ both equalise $f, g : A \to B$,
+then we can construct maps between $E$ and $E'$ via the universal property
+of equalisers, and uniqueness ensures that these maps form an isomorphism.
+
+```agda
+  is-equaliser→iso
+    : {E E' : Ob}
+    → {e : Hom E A} {e' : Hom E' A}
+    → is-equaliser C f g e
+    → is-equaliser C f g e'
+    → E ≅ E'
+  is-equaliser→iso {e = e} {e' = e'} eq eq' =
+    make-iso (eq' .universal (eq .equal)) (eq .universal (eq' .equal))
+      (unique₂ eq' (eq' .equal) (pulll (eq' .factors) ∙ eq .factors) (idr _))
+      (unique₂ eq (eq .equal) (pulll (eq .factors) ∙ eq' .factors) (idr _))
+    where open is-equaliser
+```
+
+## Properties of equalisers
+
+The equaliser of the pair $(f, f) : A \to B$ always exists, and is given
+by the identity map $\id : A \to A$.
+
+```agda
+  id-is-equaliser : is-equaliser C f f id
+  id-is-equaliser .is-equaliser.equal = refl
+  id-is-equaliser .is-equaliser.universal {e' = e'} _ = e'
+  id-is-equaliser .is-equaliser.factors = idl _
+  id-is-equaliser .is-equaliser.unique p = sym (idl _) ∙ p
+```
+
+If $e : E \to A$ is an equaliser and an [[epimorphism]], then $e$ is
+an iso.
+
+```agda
+  equaliser+epi→invertible
+    : ∀ {E} {e : Hom E A}
+    → is-equaliser C f g e
+    → is-epic e
+    → is-invertible e
+```
+
+Suppose that $e$ equalises some pair $(f, g) : A \to B$. By definition,
+this means that $f \circ e = g \circ e$; however, $e$ is an epi, so
+$f = g$. This in turn means that $\id : A \to A$ can be extended into
+a map $A \to E$ via the universal property of $e$, and universality
+ensures that this extension is an isomorphism!
+
+```agda
+  equaliser+epi→invertible {f = f} {g = g} {e = e} e-equaliser e-epi =
+    make-invertible
+      (universal {e' = id} (ap₂ _∘_ f≡g refl))
+      factors
+      (unique₂ (ap₂ _∘_ f≡g refl) (pulll factors) id-comm)
+    where
+      open is-equaliser e-equaliser
+      f≡g : f ≡ g
+      f≡g = e-epi f g equal
+```
+
+
 # Categories with all equalisers
 
 We also define a helper module for working with categories that have