🚧 Working on stable algebras

src/Algebra/Properties.lagda.md

@@ -0,0 +1,99 @@
+<!--
+```agda
+open import Level
+open import Category.Instance.AmbientCategory using (Ambient)
+open import Categories.FreeObjects.Free
+open import Categories.Functor.Core
+```
+-->
+
+```agda
+module Algebra.Properties {o ℓ e} (ambient : Ambient o ℓ e) where
+  open Ambient ambient
+  open import Algebra.ElgotAlgebra ambient
+  open import Algebra.UniformIterationAlgebra ambient
+  open import Category.Construction.ElgotAlgebras ambient
+  open import Category.Construction.UniformIterationAlgebras ambient
+
+  open Equiv
+```
+
+# Properties of algebras
+This file contains some typedefs and records concerning different algebras.
+
+## Free Uniform-Iteration Algebras
+
+```agda
+  uniformForgetfulF : Functor Uniform-Iteration-Algebras C
+  uniformForgetfulF = record
+    { F₀ = λ X → Uniform-Iteration-Algebra.A X
+    ; F₁ = λ f → Uniform-Iteration-Algebra-Morphism.h f
+    ; identity = refl
+    ; homomorphism = refl
+    ; F-resp-≈ = λ x → x
+    }
+
+  -- typedef
+  FreeUniformIterationAlgebra : Obj → Set (suc o ⊔ suc ℓ ⊔ suc e)
+  FreeUniformIterationAlgebra X = FreeObject {C = C} {D = Uniform-Iteration-Algebras} uniformForgetfulF X
+```
+
+-- TODO this is an alternate characterization, prove it with lemma 18 and formalize definition 17
+## Stable Free Uniform-Iteration Algebras
+
+## Free Elgot Algebras
+
+```agda
+  elgotForgetfulF : Functor Elgot-Algebras C
+  elgotForgetfulF = record
+    { F₀ = λ X → Elgot-Algebra.A X
+    ; F₁ = λ f → Elgot-Algebra-Morphism.h f
+    ; identity = refl
+    ; homomorphism = refl
+    ; F-resp-≈ = λ x → x
+    }
+
+  -- typedef
+  FreeElgotAlgebra : Obj → Set (suc o ⊔ suc ℓ ⊔ suc e)
+  FreeElgotAlgebra X = FreeObject {C = C} {D = Elgot-Algebras} elgotForgetfulF X
+```
+
+## Free Elgot to Free Uniform Iteration
+
+```agda
+  elgot-to-uniformF : Functor Elgot-Algebras Uniform-Iteration-Algebras
+  elgot-to-uniformF = record
+    { F₀ = λ X → record { A = Elgot-Algebra.A X ; algebra = record
+      { _# = λ f → (X Elgot-Algebra.#) f
+      ; #-Fixpoint = Elgot-Algebra.#-Fixpoint X 
+      ; #-Uniformity = Elgot-Algebra.#-Uniformity X 
+      ; #-resp-≈ = Elgot-Algebra.#-resp-≈ X 
+      }}
+    ; F₁ = λ f → record { h = Elgot-Algebra-Morphism.h f ; preserves = Elgot-Algebra-Morphism.preserves f }
+    ; identity = refl
+    ; homomorphism = refl
+    ; F-resp-≈ = λ x → x
+    }
+
+{-
+TODO / NOTES:
+- Theorem 35 talks about stable free elgot algebras,
+  but it is supposed to show that Ď and K are equivalent (under assumptions).
+  This would require us being able to get FreeUniformIterationAlgebras from FreeElgotAlgebras, but the free _* doesn't type check!
+  It probably is possible to remedy it somehow, one naive way would be to do the proof of Theorem 35 twice, 
+  once for the theorem and a second time to establish the connection between ĎX and KX.
+- TODO talk to Sergey about this
+-}
+  FreeElgot⇒FreeUniformIteration : ∀ {X} → FreeElgotAlgebra X → FreeUniformIterationAlgebra X
+  FreeElgot⇒FreeUniformIteration {X} free-elgot = record 
+    { FX = F₀ elgot 
+    ; η = η' 
+    ; _* = λ {Y} f → F₁ (f *') 
+    ; *-lift = {!   !}
+    ; *-uniq = {!   !}
+    }
+    where
+      open FreeObject free-elgot renaming (FX to elgot; η to η'; _* to _*'; *-lift to *-lift'; *-uniq to *-uniq')
+      open Elgot-Algebra elgot
+      open Functor elgot-to-uniformF using (F₀; F₁)
+```

src/Monad/Instance/K.lagda.md

@@ -1,17 +1,11 @@
 <!--
 ```agda
 open import Level
-open import Categories.Category.Equivalence using (StrongEquivalence)
-open import Function using (id)
 open import Categories.FreeObjects.Free
 open import Categories.Functor.Core
 open import Categories.Adjoint
 open import Categories.Adjoint.Properties
-open import Categories.Adjoint.Monadic.Crude
-open import Categories.NaturalTransformation.Core renaming (id to idN)
 open import Categories.Monad
-open import Categories.Category.Construction.EilenbergMoore
-open import Categories.Category.Slice
 open import Category.Instance.AmbientCategory using (Ambient)
 ```
 -->
@@ -34,24 +28,10 @@ In this file I explore the monad ***K*** and its properties:
 module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
   open Ambient ambient
   open import Category.Construction.UniformIterationAlgebras ambient
-  open import Algebra.UniformIterationAlgebra ambient
+  open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF)
+
   open Equiv
 
-  -- TODO move this to a different file
-
-  forgetfulF : Functor Uniform-Iteration-Algebras C
-  forgetfulF = record
-    { F₀ = λ X → Uniform-Iteration-Algebra.A X
-    ; F₁ = λ f → Uniform-Iteration-Algebra-Morphism.h f
-    ; identity = refl
-    ; homomorphism = refl
-    ; F-resp-≈ = id
-    }
-
-  -- typedef
-  FreeUniformIterationAlgebra : Obj → Set (suc o ⊔ suc ℓ ⊔ suc e)
-  FreeUniformIterationAlgebra X = FreeObject {C = C} {D = Uniform-Iteration-Algebras} forgetfulF X
-
 ```
 
 ### *Lemma 16*: definition of monad ***K***
@@ -62,10 +42,10 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
       algebras : ∀ X → FreeUniformIterationAlgebra X
 
     freeF : Functor C Uniform-Iteration-Algebras
-    freeF = FO⇒Functor forgetfulF algebras
+    freeF = FO⇒Functor uniformForgetfulF algebras
     
-    adjoint : freeF ⊣ forgetfulF
-    adjoint = FO⇒LAdj forgetfulF algebras
+    adjoint : freeF ⊣ uniformForgetfulF
+    adjoint = FO⇒LAdj uniformForgetfulF algebras
 
     K : Monad C
     K = adjoint⇒monad adjoint