src/Algebra/Properties.lagda.md

@@ -1,99 +0,0 @@
-<!--
-```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,9 +71,6 @@ 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ʳ; identityˡ to k-identityˡ)
+    open RMonad D-Kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
     open Monad D-Monad using () renaming (assoc to M-assoc; identityʳ to M-identityʳ)
     open HomReasoning
     open M C
@@ -75,67 +75,28 @@ We will now show that the following conditions are equivalent:
       ρ-epi : ∀ {X} → Epi (ρ {X})
       ρ-epi {X} = Coequalizer⇒Epi (coeqs X)
 
-      -- TODO this belongs in a different module
+      -- TODO this belongs in different module
-      module _ {X Y} (f : X ⇒ D₀ Y) where
+      ▷extend : ∀ {X} {Y} (f : X ⇒ D₀ Y) → ▷ ∘ extend f ≈ extend f ∘ ▷
-        private
+      ▷extend {X} {Y} f = {!   !}
-            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₁ = 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ˡ
-
-
-
-      ρ▷ : ∀ {X} → ρ ∘ ▷ ≈ ρ {X}
-      ρ▷ {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; coequalize-resp-≈) renaming (universal to coeq-universal; unique to coeq-unique; unique′ to coeq-unique′)
+          helper₁ : [ f , extend (▷ ∘ f) ] ∘ out ≈ extend f
-          intro-helper : D₁ π₁ ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈ idC
+          helper₁ = {!   !}
-          intro-helper = sym D-homomorphism ○ D-resp-≈ project₁ ○ D-identity
+
-          helper : ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈ ▷ ∘ now
+      -- TODO maybe needs that ρ is natural in X
-          helper = begin 
+      ρ▷ : ∀ {X} → ρ ∘ ▷ ≈ ρ {X}
-            ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
+      ρ▷ {X} = begin 
-            (out⁻¹ ∘ out) ∘ ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ (pullˡ (coalg-commutes ((Terminal.! (coalgebras X) {A = record { A = X × N ; α = _≅_.from nno-iso }})))) ⟩
+        ρ ∘ ▷ ≈⟨ coeq-universal {eq = eq'} ⟩ 
-            out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl)) ⟩
+        coequalize eq' ∘ ρ ≈⟨ ({!   !} ⟩∘⟨refl) ⟩ 
-            out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (idC ⁂ s) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym inject₂ ⟩∘⟨refl) ⟩
+        coequalize equality ∘ ρ ≈⟨ elimˡ (sym id-coequalize) ⟩ 
-            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₂) ⟩
+        where
-            out⁻¹ ∘ (i₂ ∘ ι) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym inject₁) ⟩
+          open Coequalizer (coeqs X) using (equality; coequalize; id-coequalize) renaming (universal to coeq-universal; unique to coeq-unique; unique′ to coeq-unique′)
-            out⁻¹ ∘ (i₂ ∘ ι) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ intro-center (_≅_.isoˡ out-≅) ⟩∘⟨refl) ⟩
+          eq' = begin 
-            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) ⟩
+            (ρ ∘ ▷) ∘ extend ι ≈⟨ pullʳ (▷extend ι) ⟩ 
-            out⁻¹ ∘ (i₂ ∘ out⁻¹ ∘ (idC +₁ ι) ∘ _≅_.from nno-iso) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ (pullʳ (pullˡ (pullʳ (cancelʳ (_≅_.isoʳ nno-iso)))))) ⟩
+            ρ ∘ extend ι ∘ ▷ ≈⟨ pullˡ equality ⟩
-            out⁻¹ ∘ i₂ ∘ (out⁻¹ ∘ (idC +₁ ι)) ∘ i₁ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ pullʳ +₁∘i₁) ⟩
+            (ρ ∘ D₁ π₁) ∘ ▷ ≈⟨ assoc ⟩
-            out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁ ∘ idC ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ) ⟩
+            ρ ∘ D₁ π₁ ∘ ▷ ≈⟨ sym (pullʳ (▷extend (now ∘ π₁))) ⟩
-            out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁ ≈⟨ ((refl⟩∘⟨ sym-assoc) ○ assoc²'') ⟩
+            (ρ ∘ ▷) ∘ D₁ π₁ ∎
-            ▷ ∘ now ∎
--- ⁂ ○
 
       Ď-Functor : Endofunctor C
       Ď-Functor = record
@@ -203,7 +164,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 , (begin ρ ∘ μ.η X ≈⟨ D-universal ⟩ Search-Algebra-on.α s-alg-on ∘ D₁ ρ ∎)
+      1⇒2 c-1 X = s-alg-on , {!   !}
         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)
@@ -217,11 +178,10 @@ We will now show that the following conditions are equivalent:
               ρ ≈⟨ sym identityˡ ⟩
               idC ∘ ρ ∎) 
             ; identity₂ = IsCoequalizer⇒Epi (c-1 X) (α' ∘ ▷) α' (begin 
-              (α' ∘ ▷) ∘ D₁ ρ ≈⟨ pullʳ (▷∘extend-comm (now ∘ ρ)) ⟩ 
+              (α' ∘ ▷) ∘ D₁ ρ ≈⟨ {!   !} ⟩ 
-              α' ∘ 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,11 +1,17 @@
 <!--
 ```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)
 ```
 -->
@@ -28,10 +34,24 @@ 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.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF)
+  open import Algebra.UniformIterationAlgebra ambient
-
   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***
@@ -42,10 +62,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 uniformForgetfulF algebras
+    freeF = FO⇒Functor forgetfulF algebras
     
-    adjoint : freeF ⊣ uniformForgetfulF
+    adjoint : freeF ⊣ forgetfulF
-    adjoint = FO⇒LAdj uniformForgetfulF algebras
+    adjoint = FO⇒LAdj forgetfulF algebras
 
     K : Monad C
     K = adjoint⇒monad adjoint