Fixed point theorems and endofunctor algebras

src/Category/CartesianClosed.ard

@@ -8,6 +8,8 @@
 \import Equiv
 \import Function.Meta
 \import HLevel
+\import Logic
+\import Logic.Meta
 \import Meta
 \import Paths
 \import Paths.Meta
@@ -32,12 +34,18 @@
   \func antitranpose-eq {X Y Z : Ob} (f : Hom (Bprod X Y) Z) : antitranspose (transpose f) = f
     => isAdjoint.ret_f f
 
+  \func transpose-eq {X Y Z : Ob} (g : Hom X (exp Y Z)) : transpose (antitranspose g) = g
+    => isAdjoint.f_ret g
+
   \func eval-map {Y Z : Ob} : Hom (Bprod (exp Y Z) Y) Z
     => antitranspose (id (exp Y Z))
 
   \func eval-transpose {X Y Z : Ob} (g : Hom (Bprod X Y) Z) : eval-map ∘ prodMap (transpose g) (id Y) = g
     => rewrite (inv $ RightAdjoint.adjoint_epsilon {exp Y} _) $ antitranpose-eq g
 
+  \func name {X Y : Ob} (f : Hom X Y) : Hom terminal (exp X Y)
+    => transpose $ f ∘ terminal-prod-left.hinv
+
   \func eval-map-eq {X Y : Ob} (f : Hom X Y) : eval-map ∘ prodMap (name f) (id X) ∘ pair terminalMap (id X) = f
     =>
       run {
@@ -51,9 +59,6 @@
   \func internal-comp {X Y Z : Ob} : Hom (Bprod (exp Y Z) (exp X Y)) (exp X Z)
     => transpose $ (eval-map ∘ prodMap (id (exp Y Z)) eval-map) ∘ associator
 
-  \func name {X Y : Ob} (f : Hom X Y) : Hom terminal (exp X Y)
-    => transpose $ f ∘ terminal-prod-left.hinv
-
   \func global-elements-iso {X Y : Ob} : Equiv {Hom X Y} {Hom terminal (exp X Y)} name
     => \new QEquiv {
       | ret f => (antitranspose f) ∘ terminal-prod-left.f
@@ -64,7 +69,7 @@
   \func internal-homFunctor : Functor (ProductPrecat (Precat.op {\this}) \this) \this
     => \new Functor {
       | F (X, Y) => exp X Y
-      | Func {(a, b)} {(c, d)} (f, g) => unfold at f $ transpose $ g ∘ eval-map ∘ prodMap (id _) f
+      | Func {(a, b)} {(c, d)} (f, g) => transpose $ g ∘ eval-map ∘ prodMap (id _) f
       | Func-id {(a, b)} => isAdjoint.adjointInv $ unfold $ rewrite (id-left, prod-id, id-right) idp
       | Func-o {(a1, b1)} {(a2, b2)} {(a3, b3)} {(f,g)} {(p,q)} =>
         run {
@@ -83,6 +88,52 @@
           equation
         }
     }
+
+\record NaturalNumbersObject {C : CartesianClosedPrecat} (N : C)
+  | zero : Hom C.terminal N
+  | succ : Hom N N
+
+
+{-
+- This section comes from "Diagonal arguments and Cartesian Closed Categories" by F.W. Lawvere
+- It is shown that any object with a "weak surjection" onto it has the fixed point property: all its endomorphisms have
+- a fixed point. The usual diagonal argument then is simply the contraposition of this theorem.
+- -}
+
+  \func has-fixed-point (Y : Ob) => \Pi (t : Hom Y Y) -> ∃ (y : Hom terminal Y) (t ∘ y = y)
+  \func weakly-surjective {A X Y : Ob} (g : Hom X (exp A Y))
+    => \Pi (f : Hom A Y) -> ∃ (x : Hom terminal X) (\Pi (a : Hom terminal A) -> eval-map ∘ (pair (g ∘ x) a) = f ∘ a)
+  \func Lawvere-fixed-point (Y : Ob) (weak-surjectivity : ∃ (A : Ob) (g : Hom A (exp A Y)) (w : weakly-surjective g))
+    : has-fixed-point Y
+    \elim weak-surjectivity
+      | inP (A, g, surj-g) =>
+        \let transp-g => antitranspose g  \in
+          \lam t =>
+              \let f => t ∘ transp-g ∘ (diagonal A)
+              | x => surj-g f
+              \in
+                \case\elim x \with {
+                  | inP (x, eq) =>
+                    \let eq-x => eq x
+                    | eqq : eval-map ∘ prodMap g (id A) = transp-g => rewrite (transpose-eq _) in eval-transpose transp-g
+                    | step : diagonal A ∘ x = pair x x =>
+                      pair-unique (rewrite beta1 $ rewriteI o-assoc $ rewrite (beta1, id-left) idp)
+                          (rewrite beta2 $ rewriteI o-assoc $ rewrite (beta2, id-left) idp)
+                    | goal : pair (g ∘ x) x  = prodMap g (id A) ∘ diagonal A ∘ x =>
+                      rewrite (o-assoc, step) $ rewrite pair-comp $ pair-unique (rewrite (beta1, beta1, o-assoc, beta1) idp)
+                                                                          (rewrite (beta2, beta2, id-left, beta2) idp)
+                    \in
+                  unfold f at eq-x $ rewrite (goal, inv o-assoc, inv o-assoc, eqq) at eq-x $
+                    inP (transp-g ∘ diagonal A ∘ x, rewrite (inv o-assoc, inv o-assoc) $ inv eq-x)
+                }
+
+  \func diagonal-argument {Y : Ob} (t : Hom Y Y) (no-fixed-point : \Pi (y : Hom terminal Y) -> Not (t ∘ y = y))
+    : \Pi (A : Ob) (g : Hom A (exp A Y)) -> Not (weakly-surjective g)
+    => \lam A g w =>
+        \let fix-point => Lawvere-fixed-point Y (inP (A, g, w)) t \in
+        \case\elim fix-point \with {
+          | inP (y, eq) => no-fixed-point y eq
+        }
 }
 
 \open PrecatWithBprod

src/Category/EndofunctorAlgebra.ard

@@ -0,0 +1,131 @@
+\import Arith.Int
+\import Arith.Nat
+\import Category
+\import Category.Functor
+\import Category.Limit
+\import Function.Meta
+\import Logic
+\import Logic.Meta
+\import Meta
+\import Paths
+\import Paths.Meta
+
+\record Algebra {C : Precat} (F : Functor C C)
+  | \coerce carrier : C
+  | morphism : Hom (F carrier) carrier
+
+\instance AlgebraPrecat {C : Precat} (F : Functor C C) : Precat (Algebra F)
+  | Hom X Y => \Sigma (m : C.Hom X Y) (m ∘ morphism {X} = morphism {Y} ∘ Func {F} m)
+  | id X => (id X, rewrite (id-left, Func-id {F}, id-right) idp)
+  | o (m1, eq1) (m2, eq2) => (m1 ∘ m2, rewrite (o-assoc, eq2, inv o-assoc, eq1, o-assoc, inv (Func-o {F})) idp)
+  | id-left => exts id-left
+  | id-right => exts id-right
+  | o-assoc => exts o-assoc
+
+-- CMonoid objects as initial algebras
+
+{- Lambek's theorem. If the F-algebra is initial, the carrier is a fixed point of the functor
+The proof is contained in the diagram
+ - F X  -> X
+ - |       |
+ - v       v
+ - FF X -> FX
+ - |       |
+ - v       v
+ - F X  -> X
+-}
+
+\func Lambek-fixed-point {C : Precat} (F : Functor C C)
+                         (init : initial-obj (AlgebraPrecat F))
+  : Iso {C} {F (carrier {init})} {carrier {init}} =>
+  \let | induced-algebra => \new Algebra {C} F {
+    | carrier => F (carrier {init})
+    | morphism => Func (morphism {init})
+  }
+       | s => initialMap' {_} {init} {induced-algebra}
+       | inverse-s : Hom {AlgebraPrecat F} induced-algebra init
+       => (morphism {init}, idp)
+       | id-map : Hom {AlgebraPrecat F} init init => id {AlgebraPrecat F} init
+       | comp => inverse-s ∘ {AlgebraPrecat F} {init} {induced-algebra} s
+       | comp-is-id : comp = id-map => initial-unique' {AlgebraPrecat F}
+       | comp-eq : inverse-s.1 ∘ s.1 = id (carrier {init}) =>
+         unfold at comp-is-id $ pmap (\lam (x,y) => x) comp-is-id
+       | comp-eq-f : s.1 ∘ morphism {init} = id (F (carrier {init})) => rewrite s.2 $ unfold $ rewrite (inv $ Func-o {F}, comp-eq, Func-id {F}) idp
+  \in
+    \new Iso {
+      | f => morphism {init}
+      | hinv => s.1
+      | hinv_f => comp-eq-f
+      | f_hinv => comp-eq
+    }
+
+{-
+Adamek's theorem
+
+If the precategory has an initial object 0, and if the diagram 0 -> F 0 -> ...
+has a colimit, and in addition this colimit is preserved by F, then this colimit is the carrier of the initial algebra
+-}
+
+--- A rather lengthy definition of the required diagram
+\func the-diagram {C : PrecatWithInitial} (F : Functor C C) : Functor NatSemiring C
+\cowith
+  | F => iterate-f C.initial
+  | Func {n} {m} n<=m => f-func {C} {F} n m n<=m
+  | Func-id {n} => f-func-id n
+  | Func-o {_} {_} {_} {y<=z} {x<=y} => func-o y<=z x<=y
+  \where {
+    \func iterate-f (ob : C) (n : Nat) : C
+    \elim n
+      | 0 => ob
+      | suc n => F (iterate-f ob n)
+
+    \func iterate-eq (ob : C) (n m : Nat) : iterate-f ob (m Nat.+ n) = iterate-f (iterate-f ob n) m
+    \elim n,m
+      | 0, _ => idp
+      | _, 0 => idp
+      | suc n, suc m => rewrite (iterate-eq ob n m) $ rewrite (iterate-lem {C} {F} (iterate-f ob n) m) idp
+      \where {
+        \func iterate-lem (ob : C) (n : Nat) : iterate-f (F ob) n = F (iterate-f ob n)
+        \elim n
+          | 0 => idp
+          | suc n => rewrite (iterate-lem ob n) idp
+      }
+
+    \func iterate-func (n : Nat) {a b : C} (f : Hom a b) : Hom (iterate-f a n) (iterate-f b n)
+    \elim n
+      | 0 => f
+      | suc n => Func {F} (iterate-func n f)
+
+    \func f-func (n m : Nat) (n<=m : n NatBSemilattice.<= m) : Hom (iterate-f initial n) (iterate-f initial m)
+    \elim n, m, n<=m
+      | 0, 0, _ => id C.initial
+      | 0, suc m, _ => C.initialMap
+      | suc n, suc m, n'<=m' =>
+        \let n<=m => suc<=suc.conv n'<=m' \in
+          Func {F} (f-func n m n<=m)
+      | suc n, 0, n'<=0 => absurd $ (lemma n) n'<=0
+      \where {
+        \func lemma (n : Nat) : Not (suc n NatBSemilattice.<= 0) => \lam contr => contr NatSemiring.zero<suc
+      }
+
+  \func f-func-id (n : Nat) : f-func n n (id n) = id (iterate-f initial n)
+    \elim n
+      | 0 => idp
+      | suc n => rewrite (f-func-id n, Func-id {F}) idp
+
+  \func func-o {x y z : Nat} (y<=z : y NatBSemilattice.<= z) (x<=y : x NatBSemilattice.<= y)
+    : f-func x z (y<=z ∘ x<=y) = f-func y z y<=z ∘ f-func x y x<=y
+    \elim x, y, z
+      | 0, 0, 0 => rewrite id-left idp
+      | 0, _, _ => C.initial-unique
+      | suc x, 0, 0 => absurd (x<=y NatSemiring.zero<suc)
+      | suc x, 0, suc z => absurd (x<=y NatSemiring.zero<suc)
+      | suc x, suc y, 0 => absurd (y<=z NatSemiring.zero<suc)
+      | suc x, suc y, suc z => rewriteI (Func-o {F}) $
+      \let y<=z => suc<=suc.conv y<=z
+      | x<=y => suc<=suc.conv x<=y \in
+      rewrite (func-o {_} {_} {x} {y} {z} y<=z x<=y) idp
+  }
+
+\func Adamek-theorem {C : PrecatWithInitial} (F : Functor C C) (has-limit : Colimit (the-diagram F))
+  (f-preserves : PreservesLimit F (the-diagram F)) : {?}

src/Category/Limit.ard

@@ -509,6 +509,7 @@
   \func map {z : C} (g : Hom z y) : Hom (pullback f g) x => pbProj1 {pullback f g}
 
 \meta terminal-obj C => Product {Empty} {C} absurd
+\meta initial-obj C => terminal-obj (Precat.op {C})
 
 \func terminal-obj-iso {C : Precat} (a b : terminal-obj C) : Iso {C} {a} {b}
 \cowith
@@ -517,8 +518,13 @@
   | hinv_f => tupleEq (\case __)
   | f_hinv => tupleEq (\case __)
 
+\func initial-obj-iso {C : Precat} (a b : initial-obj C) : Iso {C} {a} {b}
+  => Iso.op {terminal-obj-iso {Precat.op {C}} b a}
+
 \func terminalMap' {C : Precat} {t : terminal-obj C} {x : C} : Hom x t => tupleMap (\case __)
 
+\func initialMap' {C : Precat} {i : initial-obj C} {x : C} : Hom i x => terminalMap' {Precat.op {C}}
+
 \func isTerminal {C : Precat} (a : C) (e : \Pi (b : C) -> Contr (Hom b a))
   : terminal-obj C a
   \cowith
@@ -529,6 +535,9 @@
 
 \lemma terminal-unique' {C : Precat} {terminal : terminal-obj C} {x : C} {f g : Hom x terminal} : f = g => tupleEq (\case __)
 
+\lemma initial-unique' {C : Precat} {initial : initial-obj C} {x : C} {f g : Hom initial x} : f = g
+  => terminal-unique' {Precat.op {C}}
+
 \func terminal-prop {C : Cat} : isProp (terminal-obj C)
   => \lam a a' => exts (C.univalence.ret (unfold $ terminal-obj-iso a a'), \lam j => absurd j, \lam {Z} f => terminal-unique')
 
@@ -545,6 +554,14 @@
       | hinv_f => terminal-unique
 }
 
+\class PrecatWithInitial \extends Precat {
+  | initial : terminal-obj (op {\this})
+
+  \func initialMap {x : Ob} : Hom initial x => terminalMap' {op {\this}}
+  \lemma initial-unique {x : Ob} {f g : Hom initial x} : f = g
+    => terminal-unique' {op {\this}}
+}
+
 \class PrecatWithBprod \extends Precat {
   | Bprod (x y : Ob) : Product (x :: y :: nil)