General adjoint functor theorem (#433)

Proof from the nLab using joint equalisers and weakly initial objects.
Only 3.3.2 and 3.3.3 from Borceux

src/Borceux.lagda.md

@@ -49,6 +49,7 @@ open import Cat.Diagram.Limit.Finite
 open import Cat.Functor.Conservative
 open import Cat.Functor.Hom.Coyoneda
 open import Cat.Diagram.Coequaliser
+open import Cat.Functor.Adjoint.AFT
 open import Cat.Functor.Adjoint.Hom
 open import Cat.Functor.Adjoint.Kan
 open import Cat.Functor.Equivalence
@@ -670,6 +671,16 @@ _ = right-adjoint-is-continuous
 
 ### 3.3 The adjoint functor theorem
 
+<!--
+```agda
+_ = Solution-set
+_ = solution-set→left-adjoint
+```
+-->
+
+* Definition 3.3.2: `Solution-set`{.Agda}
+* Theorem 3.3.3: `solution-set→left-adjoint`{.Agda}
+
 ### 3.4 Fully faithful adjoint functors
 
 <!--

src/Cat/Diagram/Equaliser/Joint.lagda.md

@@ -0,0 +1,173 @@
+<!--
+```agda
+open import Cat.Diagram.Limit.Base
+open import Cat.Prelude
+
+import Cat.Reasoning as Cat
+```
+-->
+
+```agda
+module Cat.Diagram.Equaliser.Joint {o ℓ} (C : Precategory o ℓ) where
+```
+
+<!--
+```agda
+open Functor
+open Cat C
+open _=>_
+```
+-->
+
+# Joint equalisers {defines="joint-equaliser"}
+
+The **joint equaliser** of a family $(F_i : \hom(a, b))_i$ of parallel
+maps is a straightforward generalisation of the notion of [[equaliser]]
+to more than two maps. The universal property is straightforward to
+state: the joint equaliser of the $F_i$ is an arrow $e : E \to a$,
+satisfying $F_i e = F_j e$, which is universal with this property.
+
+```agda
+record is-joint-equaliser {ℓ'} {I : Type ℓ'} {E x y} (F : I → Hom x y) (equ : Hom E x) : Type (o ⊔ ℓ ⊔ ℓ') where
+  field
+    equal     : ∀ {i j} → F i ∘ equ ≡ F j ∘ equ
+    universal : ∀ {E'} {e' : Hom E' x} (eq : ∀ i j → F i ∘ e' ≡ F j ∘ e') → Hom E' E
+    factors   : ∀ {E'} {e' : Hom E' x} {eq : ∀ i j → F i ∘ e' ≡ F j ∘ e'} → equ ∘ universal eq ≡ e'
+    unique
+      : ∀ {E'} {e' : Hom E' x} {eq : ∀ i j → F i ∘ e' ≡ F j ∘ e'} {o : Hom E' E}
+      → equ ∘ o ≡ e'
+      → o ≡ universal eq
+```
+
+<!--
+```agda
+  unique₂
+    : ∀ {E'} {e' : Hom E' x} {o1 o2 : Hom E' E}
+    → (∀ i j → F i ∘ e' ≡ F j ∘ e')
+    → equ ∘ o1 ≡ e'
+    → equ ∘ o2 ≡ e'
+    → o1 ≡ o2
+  unique₂ eq p q = unique {eq = eq} p ∙ sym (unique q)
+```
+-->
+
+A simple calculation tells us that joint equalisers are [[monic]], much
+like binary equalisers:
+
+```agda
+  is-joint-equaliser→is-monic : is-monic equ
+  is-joint-equaliser→is-monic g h x = unique₂ (λ i j → extendl equal) refl (sym x)
+```
+
+<!--
+```agda
+record Joint-equaliser {ℓ'} {I : Type ℓ'} {x y} (F : I → Hom x y) : Type (o ⊔ ℓ ⊔ ℓ') where
+  field
+    {apex} : Ob
+    equ : Hom apex x
+    has-is-je : is-joint-equaliser F equ
+  open is-joint-equaliser has-is-je public
+
+open is-joint-equaliser
+```
+-->
+
+## Computation
+
+Joint equalisers are also limits. We can define the figure shape that
+they are limits over as a straightforward generalisation of the
+parallel-arrows category, where there is an arbitrary [[set]] of arrows
+between the two objects.
+
+```agda
+module _ {ℓ'} {I : Type ℓ'} ⦃ _ : H-Level I 2 ⦄ {x y} (F : I → Hom x y) where
+  private module P = Precategory
+
+  private
+    shape : Precategory _ _
+    shape .P.Ob              = Bool
+    shape .P.Hom false false = Lift ℓ' ⊤
+    shape .P.Hom false true  = I
+    shape .P.Hom true false  = Lift ℓ' ⊥
+    shape .P.Hom true true   = Lift ℓ' ⊤
+```
+
+<details>
+<summary>Giving this the structure of a category is trivial: other than
+the $I$-many parallel arrows, there is nothing to compose
+with.</summary>
+
+```agda
+    shape .P.Hom-set true true = hlevel 2
+    shape .P.Hom-set true false = hlevel 2
+    shape .P.Hom-set false true = hlevel 2
+    shape .P.Hom-set false false = hlevel 2
+    shape .P.id {true} = _
+    shape .P.id {false} = _
+    shape .P._∘_ {true}  {true}  {true}  f g = lift tt
+    shape .P._∘_ {false} {true}  {true}  f g = g
+    shape .P._∘_ {false} {false} {true}  f g = f
+    shape .P._∘_ {false} {false} {false} f g = lift tt
+    shape .P.idr {true}  {true}  f = refl
+    shape .P.idr {false} {true}  f = refl
+    shape .P.idr {false} {false} f = refl
+    shape .P.idl {true}  {true}  f = refl
+    shape .P.idl {false} {true}  f = refl
+    shape .P.idl {false} {false} f = refl
+    shape .P.assoc {true}  {true}  {true}  {true}  f g h = refl
+    shape .P.assoc {false} {true}  {true}  {true}  f g h = refl
+    shape .P.assoc {false} {false} {true}  {true}  f g h = refl
+    shape .P.assoc {false} {false} {false} {true}  f g h = refl
+    shape .P.assoc {false} {false} {false} {false} f g h = refl
+```
+
+</details>
+
+The family of arrows $I \to \hom(x, y)$ extends straightforwardly to a
+functor from this `shape`{.Agda} category to $\cC$.
+
+```agda
+    diagram : Functor shape C
+    diagram .F₀ true  = y
+    diagram .F₀ false = x
+    diagram .F₁ {true} {true} f = id
+    diagram .F₁ {false} {true} i = F i
+    diagram .F₁ {false} {false} f = id
+    diagram .F-id {true} = refl
+    diagram .F-id {false} = refl
+    diagram .F-∘ {true} {true} {true} f g = introl refl
+    diagram .F-∘ {false} {true} {true} f g = introl refl
+    diagram .F-∘ {false} {false} {true} f g = intror refl
+    diagram .F-∘ {false} {false} {false} f g = introl refl
+```
+
+If the family is pointed, and the `diagram`{.Agda} has a limit, then
+this limit is a joint equaliser of the given arrows. The requirement for
+a point in the family ensures that we're not taking the joint equaliser
+of *no* arrows, which would be a [[product]]. Finally, since joint
+equalisers are unique, this construction is invariant under the chosen
+point; it would thus suffice for the family to be inhabited instead.
+
+```agda
+  is-limit→joint-equaliser : ∀ {L} {l} → I → is-limit diagram L l → is-joint-equaliser F (l .η false)
+  is-limit→joint-equaliser {L} {l} ix lim = je where
+    module l = is-limit lim
+    je : is-joint-equaliser F (l .η false)
+    je .equal = sym (l .is-natural false true _) ∙ l .is-natural false true _
+    je .universal {E'} {e'} eq = l.universal
+      (λ { true → F ix ∘ e' ; false → e' })
+      λ { {true}  {true}  f → eliml refl
+        ; {false} {true}  f → eq f ix
+        ; {false} {false} f → eliml refl }
+    je .factors = l.factors _ _
+    je .unique p = l.unique _ _ _ λ where
+      true  → ap₂ _∘_ (intror refl ∙ l .is-natural false true ix) refl ∙ pullr p
+      false → p
+
+  open Joint-equaliser
+
+  Limit→Joint-equaliser : I → Limit diagram → Joint-equaliser F
+  Limit→Joint-equaliser ix lim .apex = Limit.apex lim
+  Limit→Joint-equaliser ix lim .equ = Limit.cone lim .η false
+  Limit→Joint-equaliser ix lim .has-is-je = is-limit→joint-equaliser ix (Limit.has-limit lim)
+```

src/Cat/Diagram/Initial/Weak.lagda.md

@@ -0,0 +1,163 @@
+<!--
+```agda
+open import Cat.Diagram.Equaliser.Joint
+open import Cat.Diagram.Limit.Equaliser
+open import Cat.Diagram.Product.Indexed
+open import Cat.Diagram.Limit.Product
+open import Cat.Diagram.Limit.Base
+open import Cat.Diagram.Equaliser
+open import Cat.Diagram.Initial
+open import Cat.Prelude
+
+import Cat.Reasoning as Cat
+```
+-->
+
+```agda
+module Cat.Diagram.Initial.Weak where
+```
+
+# Weakly initial objects and families {defines="weakly-initial-object"}
+
+<!--
+```agda
+module _ {o ℓ} (C : Precategory o ℓ) where
+  open Cat C
+```
+-->
+
+A **weakly initial object** is like an [[initial object]], but dropping
+the requirement of uniqueness. Explicitly, an object $X$ is weakly
+initial in $\cC$, if, for every $Y : \cC$, there merely exists an arrow
+$X \to Y$.
+
+```agda
+  is-weak-initial : ⌞ C ⌟ → Type _
+  is-weak-initial X = ∀ Y → ∥ Hom X Y ∥
+```
+
+::: {.definition #weakly-initial-family}
+We can weaken this even further, by allowing a family of objects rather
+than the single object $X$: a family $(F_i)_{i : I}$ is weakly initial
+if, for every $Y$, there exists a $j : I$ and a map $F_j \to Y$. Note
+that we don't (can't!) impose any compatibility conditions between the
+choices of indices.
+
+```agda
+  is-weak-initial-fam : ∀ {ℓ'} {I : Type ℓ'} (F : I → ⌞ C ⌟) → Type _
+  is-weak-initial-fam {I = I} F = (Y : ⌞ C ⌟) → ∃[ i ∈ I ] (Hom (F i) Y)
+```
+:::
+
+The connection between these notions is the following: the [[indexed
+product]] of a weakly initial family $F$ is a weakly initial object.
+
+```agda
+  is-wif→is-weak-initial
+    : ∀ {ℓ'} {I : Type ℓ'} (F : I → ⌞ C ⌟) {ΠF} {πf : ∀ i → Hom ΠF (F i)}
+    → is-weak-initial-fam F
+    → is-indexed-product C F πf
+    → (y : ⌞ C ⌟) → ∥ Hom ΠF y ∥
+  is-wif→is-weak-initial F {πf = πf} wif ip y = do
+    (ix , h) ← wif y
+    pure (h ∘ πf ix)
+```
+
+We can also connect these notions to the non-weak initial objects.
+Suppose $\cC$ has all [[equalisers]], including [[joint equalisers]] for
+small families. If $X$ is a weakly initial object, then the domain of
+the joint equaliser $i : L \to X$ of all arrows $X \to X$ is an initial object.
+
+```agda
+  is-weak-initial→equaliser
+    : ∀ (X : ⌞ C ⌟) {L} {l : Hom L X}
+    → (∀ y → ∥ Hom X y ∥)
+    → is-joint-equaliser C {I = Hom X X} (λ x → x) l
+    → has-equalisers C
+    → is-initial C L
+  is-weak-initial→equaliser X {L} {i} is-wi lim eqs y = contr cen (p' _) where
+    open is-joint-equaliser lim
+```
+
+Since, for any $Y$, the space of maps $e \to Y$ is inhabited, it will
+suffice to show that it is a [[proposition]]. To this end, given two
+arrows $f, g : L \to Y$, consider their equaliser $j : E \to L$. First,
+we have some arrow $k : X \to E$.
+
+```agda
+    p' : is-prop (Hom L y)
+    p' f g = ∥-∥-out! do
+      let
+        module fg = Equaliser (eqs f g)
+        open fg renaming (equ to j) using ()
+
+      k ← is-wi fg.apex
+```
+
+Then, we can calculate: as maps $L \to X$, we have $i = ijki$;
+
+```agda
+      let
+        p =
+          i               ≡⟨ introl refl ⟩
+          id ∘ i          ≡⟨ equal {j = i ∘ j ∘ k} ⟩
+          (i ∘ j ∘ k) ∘ i ≡⟨ pullr (pullr refl) ⟩
+          i ∘ j ∘ k ∘ i   ∎
+```
+
+Then, since a joint equaliser is a [[monomorphism]], we can cancel $i$
+from both sides to get $jki = \id$;
+
+```agda
+        r : j ∘ k ∘ i ≡ id
+        r = is-joint-equaliser→is-monic (j ∘ k ∘ i) id (sym p ∙ intror refl)
+```
+
+Finally, if we have $g, h : L \to Z$ with $gj = hj$, then we can
+calculate $$g = gjki = hjki = h$$, so $j$ is an [[epimorphism]]. So,
+since $j$ equalises $f$ and $g$ by construction, we have $f = g$!
+
+```agda
+        s : is-epic j
+        s g h α = intror r ∙ extendl α ∙ elimr r
+
+      pure (s f g fg.equal)
+
+    cen : Hom L y
+    cen = ∥-∥-out p' ((_∘ i) <$> is-wi y)
+```
+
+Putting this together, we can show that, if a [[complete category]] has
+a small weakly initial family indexed by a [[set]], then it has an
+initial object.
+
+```agda
+  is-complete-weak-initial→initial
+    : ∀ {I : Type ℓ} (F : I → ⌞ C ⌟) ⦃ _ : ∀ {n} → H-Level I (2 + n) ⦄
+    → is-complete ℓ ℓ C
+    → is-weak-initial-fam F
+    → Initial C
+  is-complete-weak-initial→initial F compl wif = record { has⊥ = equal-is-initial } where
+```
+
+<details>
+<summary>The proof is by pasting together the results above.</summary>
+
+```agda
+    open Indexed-product
+
+    prod : Indexed-product C F
+    prod = Limit→IP C (hlevel 3) F (compl _)
+
+    prod-is-wi : is-weak-initial (prod .ΠF)
+    prod-is-wi = is-wif→is-weak-initial F wif (prod .has-is-ip)
+
+    equal : Joint-equaliser C {I = Hom (prod .ΠF) (prod .ΠF)} λ h → h
+    equal = Limit→Joint-equaliser C _ id (is-complete-lower ℓ ℓ lzero ℓ compl _)
+    open Joint-equaliser equal using (has-is-je)
+
+    equal-is-initial = is-weak-initial→equaliser _ prod-is-wi has-is-je λ f g →
+      Limit→Equaliser C (is-complete-lower ℓ ℓ lzero lzero compl _)
+```
+
+</details>