Knaster-Tarski for categories (#436)

# Description

This PR proves a Knaster-Tarski theorem for categories, and uses it to
prove the usual Knaster-Tarski theorem for suplattices.

## Checklist

Before submitting a merge request, please check the items below:

- [x] I've read [the contributing
guidelines](https://github.com/plt-amy/1lab/blob/main/CONTRIBUTING.md).
- [x] The imports of new modules have been sorted with
`support/sort-imports.hs` (or `nix run --experimental-features
nix-command -f . sort-imports`).
- [x] All new code blocks have "agda" as their language.

If your change affects many files without adding substantial content,
and
you don't want your name to appear on those pages (for example, treewide
refactorings or reformattings), start the commit message and PR title
with `chore:`.

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

@@ -133,11 +133,11 @@ initial object.
 
 ```agda
   is-complete-weak-initial→initial
-    : ∀ {I : Type ℓ} (F : I → ⌞ C ⌟) ⦃ _ : ∀ {n} → H-Level I (2 + n) ⦄
-    → is-complete ℓ ℓ C
+    : ∀ {κ} {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
+  is-complete-weak-initial→initial {κ = κ} F compl wif = record { has⊥ = equal-is-initial } where
 ```
 
 <details>
@@ -147,17 +147,17 @@ initial object.
     open Indexed-product
 
     prod : Indexed-product C F
-    prod = Limit→IP C (hlevel 3) F (compl _)
+    prod = Limit→IP C (hlevel 3) F (is-complete-lower κ ℓ κ κ 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 _)
+    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 _)
+      Limit→Equaliser C (is-complete-lower κ (ℓ ⊔ κ) lzero lzero compl _)
 ```
 
 </details>

src/Cat/Functor/Adjoint/AFT.lagda.md

@@ -16,7 +16,7 @@ import Cat.Reasoning as Cat
 module Cat.Functor.Adjoint.AFT where
 ```
 
-# The adjoint functor theorem
+# The adjoint functor theorem {defines="adjoint-functor-theorem"}
 
 The **adjoint functor theorem** states a sufficient condition for a
 [[continuous functor]] $F : \cC \to \cD$ from a locally small,

src/Cat/Functor/Algebra.lagda.md

@@ -38,8 +38,8 @@ module _ {o ℓ} {C : Precategory o ℓ} (F : Functor C C) where
 
 <!--
 ```agda
+  private module F = Cat.Functor.Reasoning F
   open Cat.Reasoning C
-  module F = Cat.Functor.Reasoning F
   open Displayed
   open Total-hom
 ```

src/Cat/Functor/Algebra/KnasterTarski.lagda.md

@@ -0,0 +1,185 @@
+---
+description: |
+  The Knaster-Tarski theorem for categories.
+---
+<!--
+```agda
+open import Cat.Functor.Algebra.Limits
+open import Cat.Diagram.Initial.Weak
+open import Cat.Diagram.Limit.Base
+open import Cat.Diagram.Initial
+open import Cat.Displayed.Total
+open import Cat.Functor.Algebra
+open import Cat.Prelude
+
+open import Order.Diagram.Fixpoint
+open import Order.Diagram.Glb
+open import Order.Base
+open import Order.Cat
+
+import Cat.Reasoning
+```
+-->
+```agda
+module Cat.Functor.Algebra.KnasterTarski where
+```
+
+# The Knaster-Tarski fixpoint theorem {defines="knaster-tarski"}
+
+The **Knaster-Tarski theorem** gives a recipe for constructing [[initial]]
+[[F-algebras]] in [[complete categories]].
+
+The big idea is that if a category $\cC$ is complete, then we can construct
+an initial algebra of a functor $F$ by taking a limit $\rm{Fix}$ over the forgetful
+functor $\pi : \FAlg{F} \to \cC$ from the category of $F$-algebras:
+the universal property of such a limit let us construct an algebra
+$F(\rm{Fix}) \to \rm{Fix}$, and the projections out of $\rm{Fix}$ let
+us establish that $\rm{Fix}$ is the initial algebra.
+
+Unfortunately, this limit is a bit too ambitious. If we examine the universe
+levels involved, we will quickly notice that this argument requires $\cC$
+to admit limits indexed by the \emph{objects} of $\cC$, which in the presence
+of excluded middle means that $\cC$ must be a preorder.
+
+This problem of overly ambitious limits is similar to the one encountered
+in the naïve [[adjoint functor theorem]], so we can use a similar technique
+to repair our proof. In particular, we will impose a variant of the
+**solution set condition** on the category of $F$-algebras that ensures
+that the limit we end up computing is determined by a small amount of data,
+which lets us relax our large-completeness requirement.
+
+More precisely, we will require that the category of $F$-algebras has a
+small [[weakly initial family]] of algebras. This means that we need:
+
+- A family $\alpha_i : F(A_i) \to A_i$ of $F$ algebras indexed by a
+  small set $I$, such that;
+- For every $F$-algebra $\beta : F(B) \to B$, there (merely) exists an $i : I$
+  along with a $F$-algebra morphism $A_i \to B$.
+
+<!--
+```agda
+module _
+  {o ℓ} {C : Precategory o ℓ}
+  (F : Functor C C)
+  where
+  open Cat.Reasoning C
+  open Functor F
+  open Total-hom
+```
+-->
+
+Once we have a solution set, the theorem pops open like a walnut submerged
+in water:
+
+* First, $\cC$ is small-complete, so the category of $F$-algebras must also
+  be small-complete, as [[limits of algebras]] are computed by limits
+  in $\cC$.
+* In particular, the category of $F$-algebras has all small [[equalisers]],
+  so we can upgrade our weakly initial family to an [[initial object]].
+
+```agda
+  solution-set→initial-algebra
+    : ∀ {κ} {Idx : Type κ} ⦃ _ : ∀ {n} → H-Level Idx (2 + n) ⦄
+    → (Aᵢ : Idx → FAlg.Ob F)
+    → is-complete κ (ℓ ⊔ κ) C
+    → is-weak-initial-fam (FAlg F) Aᵢ
+    → Initial (FAlg F)
+  solution-set→initial-algebra Aᵢ complete soln-set =
+    is-complete-weak-initial→initial (FAlg F)
+      Aᵢ
+      (FAlg-is-complete complete F)
+      soln-set
+```
+
+We can obtain the more familiar form of the Knaster-Tarski theorem by
+applying [[Lambek's lemma]] to the resulting initial algebra.
+
+```agda
+  solution-set→fixpoint
+    : ∀ {κ} {Idx : Type κ} ⦃ _ : ∀ {n} → H-Level Idx (2 + n) ⦄
+    → (Aᵢ : Idx → FAlg.Ob F)
+    → is-complete κ (ℓ ⊔ κ) C
+    → is-weak-initial-fam (FAlg F) Aᵢ
+    → Σ[ Fix ∈ Ob ] (F₀ Fix ≅ Fix)
+  solution-set→fixpoint Aᵢ complete soln-set =
+    bot .fst , invertible→iso (bot .snd) (lambek F (bot .snd) has⊥)
+    where open Initial (solution-set→initial-algebra Aᵢ complete soln-set)
+```
+
+## Knaster-Tarski for sup-lattices
+
+<!--
+```agda
+module _
+  {o ℓ} (P : Poset o ℓ)
+  (f : Monotone P P)
+  where
+  open Poset P
+  open Total-hom
+```
+-->
+
+The "traditional" Knaster-Tarski theorem states that every [[monotone endomap|monotone-map]]
+on a [[poset]] $P$ with all [[greatest lower bounds]] has a [[least fixpoint]].
+In the presence of [[propositional resizing]], this theorem follows as a corollary of
+our previous theorem.
+
+```agda
+  complete→least-fixpoint
+    : (∀ {I : Type o} → (k : I → Ob) → Glb P k)
+    → Least-fixpoint P f
+  complete→least-fixpoint glbs = least-fixpoint where
+```
+
+<!--
+```agda
+    open Cat.Reasoning (poset→category P) using (_≅_; to; from)
+    open is-least-fixpoint
+    open Least-fixpoint
+```
+-->
+
+The key is that resizing lets us prove the solution set condition with
+respect to the size of the underlying set of $P$, as we can resize away
+the proofs that $f x \leq x$.
+
+```agda
+    Idx : Type o
+    Idx = Σ[ x ∈ Ob ] (□ (f # x ≤ x))
+
+    soln : Idx → Σ[ x ∈ Ob ] (f # x ≤ x)
+    soln (x , lt) = x , (□-out! lt)
+
+    is-soln-set : is-weak-initial-fam (FAlg (monotone→functor f)) soln
+    is-soln-set (x , lt) = inc ((x , inc lt) , total-hom ≤-refl prop!)
+```
+
+Moreover, $P$ has all [[greatest lower bounds]], so it is `complete as a
+category`{.Agda ident=glbs→complete}. This lets us invoke the general
+Knaster-Tarski theorem to get an initial $f$-algebra.
+
+```agda
+    initial : Initial (FAlg (monotone→functor f))
+    initial =
+      solution-set→initial-algebra (monotone→functor f)
+        soln
+        (glbs→complete glbs)
+        is-soln-set
+```
+
+Finally, we can inline the proof of [[Lambek's lemma]] to show that this
+initial algebra gives the least fixpoint of $f$!
+
+```agda
+    open Initial initial
+
+    least-fixpoint : Least-fixpoint P f
+    least-fixpoint .fixpoint =
+      bot .fst
+    least-fixpoint .has-least-fixpoint .fixed =
+      ≤-antisym
+        (bot .snd)
+        (¡ {x = f .hom (bot .fst) , f .pres-≤ (bot .snd)} .hom)
+    least-fixpoint .has-least-fixpoint .least x fx=x =
+      ¡ {x = x , ≤-refl' fx=x} .hom
+```

src/Cat/Functor/Algebra/Limits.lagda.md

@@ -0,0 +1,121 @@
+---
+description: |
+  Limits in categories of F-algebras.
+---
+<!--
+```agda
+open import Cat.Diagram.Limit.Base
+open import Cat.Displayed.Total
+open import Cat.Functor.Algebra
+open import Cat.Prelude
+
+import Cat.Functor.Reasoning
+import Cat.Reasoning
+```
+-->
+```agda
+module Cat.Functor.Algebra.Limits where
+```
+
+# Limits in categories of algebras {defines="limits-of-algebras"}
+
+This short note details the construction of [[limits]] in categories of
+[[F-algebras]] from limits in the underlying category.
+
+<!-- [TODO: Reed M, 17/10/2024]
+This should really be about creation of limits/display, but I don't want to deal
+with that at the moment!
+-->
+
+<!--
+```agda
+module _
+  {o ℓ oj ℓj} {C : Precategory o ℓ}
+  (F : Functor C C)
+  {J : Precategory oj ℓj} (K : Functor J (FAlg F))
+  where
+  open Cat.Reasoning C
+  private
+    module J = Cat.Reasoning J
+    module F = Cat.Functor.Reasoning F
+    module K = Cat.Functor.Reasoning K
+  open Total-hom
+```
+-->
+
+Let $F : \cC \to \cC$ be an endofunctor, and $K : \cJ \to \FAlg{F}$ be a
+diagram of $F$-algebras. If $\cC$ has a limit $L$ of $\pi \circ K$, then
+$F(L)$ is the limit of $K$ in $\FAlg{F}$.
+
+
+```agda
+  Forget-algebra-lift-limit : Limit (πᶠ (F-Algebras F) F∘ K) → Limit K
+  Forget-algebra-lift-limit L = to-limit (to-is-limit L') where
+    module L = Limit L
+    open make-is-limit
+```
+
+As noted earlier, the underlying object of the limit is $F(L)$. The algebra
+$F(L) \to L$ is constructed via the universal property of $L$: to
+give a map $F(L) \to L$, it suffices to give maps $F(L) \to K(j)$ for
+every $j : \cJ$, which we can construct by composing the projection
+$F(\psi_{j}) : F(L) \to F(K(j))$ with the algebra $F(K(j)) \to K(j)$.
+
+```agda
+    apex : FAlg.Ob F
+    apex .fst = L.apex
+    apex .snd = L.universal (λ j → K.₀ j .snd ∘ F.₁ (L.ψ j)) comm where abstract
+      comm
+        : ∀ {i j : J.Ob} (f : J.Hom i j)
+        → K.₁ f .hom ∘ K.₀ i .snd ∘ F.₁ (L.ψ i) ≡ K.₀ j .snd ∘ F.₁ (L.ψ j)
+      comm {i} {j} f =
+        K.₁ f .hom ∘ K.₀ i .snd ∘ F.₁ (L.ψ i)         ≡⟨ pulll (K.₁ f .preserves) ⟩
+        (K.₀ j .snd ∘ F.₁ (K.₁ f .hom)) ∘ F.₁ (L.ψ i) ≡⟨ F.pullr (L.commutes f) ⟩
+        K.₀ j .snd ∘ F.₁ (L.ψ j)                      ∎
+```
+
+A short series of calculations shows that the projections and universal map
+associated to $L$ are $F$-algebra homomorphisms.
+
+```agda
+    L' : make-is-limit K apex
+    L' .ψ j .hom = L.ψ j
+    L' .ψ j .preserves = L.factors _ _
+    L' .universal eps p .hom =
+      L.universal (λ j → eps j .hom) (λ f → ap hom (p f))
+    L' .universal eps p .preserves =
+      L.unique₂ (λ j → K.F₀ j .snd ∘ F.₁ (eps j .hom))
+        (λ f → pulll (K.₁ f .preserves) ∙ F.pullr (ap hom (p f)))
+        (λ j → pulll (L.factors _ _) ∙ eps j .preserves)
+        (λ j → pulll (L.factors _ _) ∙ F.pullr (L.factors _ _))
+```
+
+Finally, equality of morphisms of $F$-algebras is given by equality on
+the underlying morphisms, so all of the relevant diagrams in $\FAlg{F}$
+commute.
+
+```agda
+    L' .commutes f =
+      total-hom-path (F-Algebras F) (L.commutes f) prop!
+    L' .factors eps p =
+      total-hom-path (F-Algebras F) (L.factors _ _) prop!
+    L' .unique eps p other q =
+      total-hom-path (F-Algebras F) (L.unique _ _ _ λ j → ap hom (q j)) prop!
+```
+
+<!--
+```agda
+module _
+  {o ℓ oκ ℓκ} {C : Precategory o ℓ}
+  (complete : is-complete oκ ℓκ C)
+  where
+```
+-->
+
+This gives us the following useful corollary: if $\cC$ is $\kappa$-complete,
+then $\FAlg{F}$ is also $\kappa$ complete.
+
+```agda
+  FAlg-is-complete : (F : Functor C C) → is-complete oκ ℓκ (FAlg F)
+  FAlg-is-complete F K = Forget-algebra-lift-limit F K (complete (πᶠ (F-Algebras F) F∘ K))
+```

src/Order/Cat.lagda.md

@@ -59,14 +59,18 @@ automatic.
 
 ```agda
 open Functor
-Posets↪Strict-cats : ∀ {ℓ ℓ'} → Functor (Posets ℓ ℓ') (Strict-cats ℓ ℓ')
-Posets↪Strict-cats .F₀ P = poset→category P , Poset.Ob-is-set P
 
-Posets↪Strict-cats .F₁ f .F₀ = f .hom
-Posets↪Strict-cats .F₁ f .F₁ = f .pres-≤
-Posets↪Strict-cats .F₁ {y = y} f .F-id    = Poset.≤-thin y _ _
-Posets↪Strict-cats .F₁ {y = y} f .F-∘ g h = Poset.≤-thin y _ _
+monotone→functor
+  : ∀ {o ℓ o' ℓ'} {P : Poset o ℓ} {Q : Poset o' ℓ'}
+  → Monotone P Q → Functor (poset→category P) (poset→category Q)
+monotone→functor f .F₀ = f .hom
+monotone→functor f .F₁ = f .pres-≤
+monotone→functor f .F-id = prop!
+monotone→functor f .F-∘ _ _ = prop!
 
+Posets↪Strict-cats : ∀ {ℓ ℓ'} → Functor (Posets ℓ ℓ') (Strict-cats ℓ ℓ')
+Posets↪Strict-cats .F₀ P = poset→category P , Poset.Ob-is-set P
+Posets↪Strict-cats .F₁ f = monotone→functor f
 Posets↪Strict-cats .F-id    = Functor-path (λ _ → refl) λ _ → refl
 Posets↪Strict-cats .F-∘ f g = Functor-path (λ _ → refl) λ _ → refl
 ```

src/Order/Diagram/Fixpoint.lagda.md

@@ -19,6 +19,8 @@ open Order.Reasoning P
 ```
 -->
 
+# Least fixpoints {defines="least-fixpoint"}
+
 Let $(P, \le)$ be a poset, and $f : P \to P$ be a monotone map. We say
 that $f$ has a **least fixpoint** if there exists some $x : P$ such that
 $f(x) = x$, and for every other $y$ such that $f(y) = y$, $x \le y$.