🚧 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/Delay.lagda.md

@@ -71,6 +71,9 @@ We then use Lambek's Lemma to gain an isomorphism `D X ≅ X + D X`, whose inver
 
       unitlaw : out ∘ now ≈ i₁
       unitlaw = cancelˡ (_≅_.isoʳ out-≅)
+
+      laterlaw : out ∘ later ≈ i₂
+      laterlaw = cancelˡ (_≅_.isoʳ out-≅)
 ```
 
 Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use the final coalgebras to get a *coiteration operator* `coit`:

src/Monad/Instance/Delay/Quotienting.lagda.md

@@ -57,7 +57,7 @@ We will now show that the following conditions are equivalent:
     open DelayM D renaming (functor to D-Functor; monad to D-Monad; kleisli to D-Kleisli)
 
     open Functor D-Functor using () renaming (F₁ to D₁; homomorphism to D-homomorphism; F-resp-≈ to D-resp-≈; identity to D-identity)
-    open RMonad D-Kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
+    open RMonad D-Kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ; identityˡ to k-identityˡ)
     open Monad D-Monad using () renaming (assoc to M-assoc; identityʳ to M-identityʳ)
     open HomReasoning
     open M C
@@ -75,28 +75,67 @@ We will now show that the following conditions are equivalent:
       ρ-epi : ∀ {X} → Epi (ρ {X})
       ρ-epi {X} = Coequalizer⇒Epi (coeqs X)
 
-      -- TODO this belongs in different module
-      ▷extend : ∀ {X} {Y} (f : X ⇒ D₀ Y) → ▷ ∘ extend f ≈ extend f ∘ ▷
-      ▷extend {X} {Y} f = {!   !}
-        where
+      -- TODO this belongs in a different module
+      module _ {X Y} (f : X ⇒ D₀ Y) where
+        private
+            helper : out ∘ [ f , extend (▷ ∘ f) ] ∘ out ≈ [ out ∘ f , i₂ ∘ [ f , extend (▷ ∘ f) ] ∘ out ] ∘ out
+            helper = pullˡ ∘[] ○ (([]-cong₂ refl (extendlaw (▷ ∘ f) ○ ((([]-cong₂ (pullˡ laterlaw) refl) ⟩∘⟨refl) ○ sym (pullˡ ∘[])))) ⟩∘⟨refl)
             helper₁ : [ f , extend (▷ ∘ f) ] ∘ out ≈ extend f
-          helper₁ = {!   !}
+            helper₁ = sym (extend'-unique f ([ f , extend (▷ ∘ f) ] ∘ out) helper)
+
+        ▷∘extendˡ : ▷ ∘ extend f ≈ extend (▷ ∘ f)
+        ▷∘extendˡ = sym (begin 
+          extend (▷ ∘ f) ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
+          (out⁻¹ ∘ out) ∘ extend (▷ ∘ f) ≈⟨ pullʳ (extendlaw (▷ ∘ f)) ⟩
+          out⁻¹ ∘ [ out ∘ ▷ ∘ f , i₂ ∘ extend (▷ ∘ f) ] ∘ out ≈⟨ (refl⟩∘⟨ (([]-cong₂ (pullˡ laterlaw) refl) ○ (sym ∘[])) ⟩∘⟨refl) ⟩
+          out⁻¹ ∘ (i₂ ∘ [ f , extend (▷ ∘ f) ]) ∘ out ≈⟨ (refl⟩∘⟨ (pullʳ helper₁)) ⟩
+          out⁻¹ ∘ i₂ ∘ extend f ≈⟨ sym-assoc ⟩
+          ▷ ∘ extend f ∎)
+
+        ▷∘extend-comm : ▷ ∘ extend f ≈ extend f ∘ ▷
+        ▷∘extend-comm = sym (begin 
+          extend f ∘ ▷ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
+          (out⁻¹ ∘ out) ∘ extend f ∘ ▷ ≈⟨ pullʳ (pullˡ (extendlaw f)) ⟩ 
+          out⁻¹ ∘ ([ out ∘ f , i₂ ∘ extend f ] ∘ out) ∘ ▷ ≈⟨ (refl⟩∘⟨ pullʳ laterlaw) ⟩ 
+          out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend f ] ∘ i₂ ≈⟨ (refl⟩∘⟨ inject₂) ○ sym-assoc ⟩ 
+          ▷ ∘ extend f ∎)
+
+        ▷∘extendʳ : extend f ∘ ▷ ≈ extend (▷ ∘ f)
+        ▷∘extendʳ = (sym ▷∘extend-comm) ○ ▷∘extendˡ
+
+
 
-      -- TODO maybe needs that ρ is natural in X
       ρ▷ : ∀ {X} → ρ ∘ ▷ ≈ ρ {X}
-      ρ▷ {X} = begin 
-        ρ ∘ ▷ ≈⟨ coeq-universal {eq = eq'} ⟩ 
-        coequalize eq' ∘ ρ ≈⟨ ({!   !} ⟩∘⟨refl) ⟩ 
-        coequalize equality ∘ ρ ≈⟨ elimˡ (sym id-coequalize) ⟩ 
-        ρ ∎
+      ρ▷ {X} = sym (begin 
+        ρ ≈⟨ introʳ intro-helper ⟩ 
+        ρ ∘ D₁ π₁ ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullˡ (sym equality) ⟩ 
+        (ρ ∘ extend ι) ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ (sym k-assoc) ⟩ 
+        ρ ∘ extend (extend ι ∘ now ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩) ≈⟨ (refl⟩∘⟨ extend-≈ (pullˡ k-identityʳ)) ⟩ 
+        ρ ∘ extend (ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩) ≈⟨ (refl⟩∘⟨ extend-≈ helper) ⟩ 
+        ρ ∘ extend (▷ ∘ now) ≈⟨ (refl⟩∘⟨ sym (▷∘extendʳ now)) ⟩ 
+        ρ ∘ extend now ∘ ▷ ≈⟨ elim-center k-identityˡ ⟩ 
+        ρ ∘ ▷ ∎)
         where
-          open Coequalizer (coeqs X) using (equality; coequalize; id-coequalize) renaming (universal to coeq-universal; unique to coeq-unique; unique′ to coeq-unique′)
-          eq' = begin 
-            (ρ ∘ ▷) ∘ extend ι ≈⟨ pullʳ (▷extend ι) ⟩ 
-            ρ ∘ extend ι ∘ ▷ ≈⟨ pullˡ equality ⟩
-            (ρ ∘ D₁ π₁) ∘ ▷ ≈⟨ assoc ⟩
-            ρ ∘ D₁ π₁ ∘ ▷ ≈⟨ sym (pullʳ (▷extend (now ∘ π₁))) ⟩
-            (ρ ∘ ▷) ∘ D₁ π₁ ∎
+          open Coequalizer (coeqs X) using (equality; coequalize; id-coequalize; coequalize-resp-≈) renaming (universal to coeq-universal; unique to coeq-unique; unique′ to coeq-unique′)
+          intro-helper : D₁ π₁ ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈ idC
+          intro-helper = sym D-homomorphism ○ D-resp-≈ project₁ ○ D-identity
+          helper : ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈ ▷ ∘ now
+          helper = begin 
+            ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
+            (out⁻¹ ∘ out) ∘ ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ (pullˡ (coalg-commutes ((Terminal.! (coalgebras X) {A = record { A = X × N ; α = _≅_.from nno-iso }})))) ⟩
+            out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl)) ⟩
+            out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (idC ⁂ s) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym inject₂ ⟩∘⟨refl) ⟩
+            out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (_≅_.to nno-iso ∘ i₂) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ (pullʳ (pullˡ (cancelˡ (_≅_.isoʳ nno-iso))))) ⟩
+            out⁻¹ ∘ (idC +₁ ι) ∘ i₂ ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ pullˡ +₁∘i₂) ⟩
+            out⁻¹ ∘ (i₂ ∘ ι) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym inject₁) ⟩
+            out⁻¹ ∘ (i₂ ∘ ι) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ intro-center (_≅_.isoˡ out-≅) ⟩∘⟨refl) ⟩
+            out⁻¹ ∘ (i₂ ∘ (out⁻¹ ∘ out) ∘ ι) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ (refl⟩∘⟨ pullʳ (coalg-commutes ((Terminal.! (coalgebras X) {A = record { A = X × N ; α = _≅_.from nno-iso }})))) ⟩∘⟨refl) ⟩
+            out⁻¹ ∘ (i₂ ∘ out⁻¹ ∘ (idC +₁ ι) ∘ _≅_.from nno-iso) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ (pullʳ (pullˡ (pullʳ (cancelʳ (_≅_.isoʳ nno-iso)))))) ⟩
+            out⁻¹ ∘ i₂ ∘ (out⁻¹ ∘ (idC +₁ ι)) ∘ i₁ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ pullʳ +₁∘i₁) ⟩
+            out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁ ∘ idC ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ) ⟩
+            out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁ ≈⟨ ((refl⟩∘⟨ sym-assoc) ○ assoc²'') ⟩
+            ▷ ∘ now ∎
+-- ⁂ ○
 
       Ď-Functor : Endofunctor C
       Ď-Functor = record
@@ -164,7 +203,7 @@ We will now show that the following conditions are equivalent:
       cond-4 = {!   !}
 
       1⇒2 : cond-1 → cond-2
-      1⇒2 c-1 X = s-alg-on , {!   !}
+      1⇒2 c-1 X = s-alg-on , (begin ρ ∘ μ.η X ≈⟨ D-universal ⟩ Search-Algebra-on.α s-alg-on ∘ D₁ ρ ∎)
         where
           open Coequalizer (coeqs X) renaming (universal to coeq-universal)
           open IsCoequalizer (c-1 X) using () renaming (equality to D-equality; coequalize to D-coequalize; universal to D-universal; unique to D-unique)
@@ -178,10 +217,11 @@ We will now show that the following conditions are equivalent:
               ρ ≈⟨ sym identityˡ ⟩
               idC ∘ ρ ∎) 
             ; identity₂ = IsCoequalizer⇒Epi (c-1 X) (α' ∘ ▷) α' (begin 
-              (α' ∘ ▷) ∘ D₁ ρ ≈⟨ {!   !} ⟩ 
-              {!   !} ≈⟨ {!   !} ⟩
-              {!   !} ≈⟨ {!   !} ⟩
-              {!   !} ≈⟨ {!   !} ⟩
+              (α' ∘ ▷) ∘ D₁ ρ ≈⟨ pullʳ (▷∘extend-comm (now ∘ ρ)) ⟩ 
+              α' ∘ D₁ ρ ∘ ▷ ≈⟨ pullˡ (sym D-universal) ⟩
+              (ρ ∘ μ.η X) ∘ ▷ ≈⟨ pullʳ (sym (▷∘extend-comm idC)) ⟩
+              ρ ∘ ▷ ∘ extend idC ≈⟨ pullˡ ρ▷ ⟩
+              ρ ∘ extend idC ≈⟨ D-universal ⟩
               α' ∘ D₁ ρ ∎) 
             }
             where

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