Knaster-Tarski for categories

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$.