🚧 Small progress, stuck on multiple fronts

src/Algebra/Properties.lagda.md

@@ -5,6 +5,11 @@ open import Level
 open import Category.Instance.AmbientCategory using (Ambient)
 open import Categories.FreeObjects.Free
 open import Categories.Functor.Core
+open import Categories.Functor.Algebra
+open import Categories.Functor.Coalgebra
+open import Categories.Object.Terminal
+open import Categories.Category.Construction.EilenbergMoore
+open import Categories.Monad.Relative renaming (Monad to RMonad)
 ```
 -->
 
@@ -15,8 +20,14 @@ module Algebra.Properties {o ℓ e} (ambient : Ambient o ℓ e) where
   open import Algebra.UniformIterationAlgebra ambient
   open import Category.Construction.ElgotAlgebras ambient
   open import Category.Construction.UniformIterationAlgebras ambient
+  open import Algebra.Search ambient
+  open import Monad.Instance.Delay ambient
+  open import Categories.Morphism.Properties C
 
   open Equiv
+  open HomReasoning
+  open MR C
+  open M C
 ```
 
 # Properties of algebras
@@ -144,3 +155,116 @@ This file contains some typedefs and records concerning different algebras.
     where
       open Functor elgot-to-uniformF
       open Functor (FO⇒Functor elgotForgetfulF free-elgots) using () renaming (F₀ to FO₀; F₁ to FO₁)
+
+
+
+## **D**-Algebra + Search-Algebra ⇒ Elgot algebra
+```agda
+  Search⇒Uniform : (D : DelayM) → Search-Algebra D → Uniform-Iteration-Algebra
+  Search⇒Uniform D S = record 
+    { A = A 
+    ; algebra = record
+      { _# = λ {X} f → α ∘ coit f
+      ; #-Fixpoint = λ {X} {f} → begin 
+        α ∘ coit f ≈⟨ intro-center (_≅_.isoˡ out-≅) ⟩ 
+        α ∘ (out⁻¹ ∘ out) ∘ coit f ≈⟨ (refl⟩∘⟨ ((sym +-g-η) ⟩∘⟨refl) ⟩∘⟨refl) ⟩ 
+        α ∘ ([ now , later ] ∘ out) ∘ coit f ≈⟨ pullˡ (pullˡ ∘[]) ⟩ 
+        ([ α ∘ now , α ∘ later ] ∘ out) ∘ coit f ≈⟨ ([]-cong₂ identity₁ identity₂ ⟩∘⟨refl ⟩∘⟨refl) ⟩ 
+        ([ idC , α ] ∘ out) ∘ coit f ≈⟨ pullʳ (coit-commutes f) ⟩ 
+        [ idC , α ] ∘ (idC +₁ coit f) ∘ f ≈⟨ pullˡ []∘+₁ ⟩ 
+        [ idC ∘ idC , α ∘ coit f ] ∘ f ≈⟨ (([]-cong₂ identity² refl) ⟩∘⟨refl) ⟩ 
+        [ idC , α ∘ coit f ] ∘ f ∎ 
+      ; #-Uniformity = λ {X} {Y} {f} {g} {h} eq → begin 
+        α ∘ coit f ≈⟨ sym (pullʳ (sym (Terminal.!-unique (coalgebras A) (record { f = coit g ∘ h ; commutes = begin 
+          out ∘ coit g ∘ h ≈⟨ pullˡ (coit-commutes g) ⟩ 
+          ((idC +₁ coit g) ∘ g) ∘ h ≈⟨ pullʳ (sym eq) ⟩ 
+          (idC +₁ coit g) ∘ (idC +₁ h) ∘ f ≈⟨ pullˡ +₁∘+₁ ⟩ 
+          (idC ∘ idC +₁ coit g ∘ h) ∘ f ≈⟨ ((+₁-cong₂ identity² refl) ⟩∘⟨refl) ⟩ 
+          (idC +₁ coit g ∘ h) ∘ f ∎ })))) ⟩ 
+        (α ∘ coit g) ∘ h ∎ 
+      ; #-resp-≈ = λ {X} {f} {g} eq → refl⟩∘⟨ coit-resp-≈ eq
+      }
+    }
+    where 
+      open Search-Algebra S
+      open DelayM D
+
+  -- TODO use IsElgot
+  D-Algebra+Search⇒Elgot : (D : DelayM) → (mod : Module (DelayM.monad D)) → IsSearchAlgebra D (Module.action mod) → Elgot-Algebra
+  D-Algebra+Search⇒Elgot D mod search = record { A = A ; algebra = record
+    { _# = _#
+    ; #-Fixpoint = #-Fixpoint
+    ; #-Uniformity = #-Uniformity
+    ; #-Folding = #-Folding'
+    ; #-resp-≈ = #-resp-≈
+    } }
+    where
+      open Module mod using (A) renaming (action to α; commute to D-commute)
+      open DelayM D
+      open IsSearchAlgebra search using ()
+      open Uniform-Iteration-Algebra (Search⇒Uniform D (IsSearchAlgebra⇒Search-Algebra D α search)) using (_#; #-Fixpoint; #-Uniformity; #-resp-≈)
+      #-Folding' : ∀ {X Y : Obj} {f : X ⇒ A + X} {h : Y ⇒ X + Y} → α ∘ DelayM.coit D (α ∘ DelayM.coit D f +₁ h) ≈ α ∘ DelayM.coit D [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]
+      #-Folding' {X} {Y} {f} {h} = 
+        begin 
+        α ∘ coit (α ∘ coit f +₁ h) ≈⟨ refl⟩∘⟨ (coit-resp-≈ (sym (+₁∘+₁ ○ +₁-cong₂ refl identityˡ))) ⟩ 
+        α ∘ coit ((α +₁ idC) ∘ (coit f +₁ h)) ≈⟨ refl⟩∘⟨ sym (helper''' (coit f +₁ h) α) ⟩ 
+        α ∘ extend (now ∘ α) ∘ coit (coit f +₁ h) ≈⟨ pullˡ D-commute ⟩ 
+        (α ∘ extend idC) ∘ coit (coit f +₁ h) ≈⟨ pullʳ (sym ([]-unique goal₁ goal₂)) ⟩
+        α ∘ [ coit f , coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ ∘[] ⟩
+        [ α ∘ coit f , α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ sym ([]-cong₂ (sym #-Fixpoint) refl) ⟩
+        [ [ idC , α ∘ coit f ] ∘ f , α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ sym ([]-cong₂ (([]-cong₂ identity² (assoc ○ helper'')) ⟩∘⟨refl) assoc) ⟩
+        [ [ idC ∘ idC , (α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₁ ] ∘ f , (α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ h ] ≈⟨ sym ([]-cong₂ (pullˡ []∘+₁) (pullˡ inject₂)) ⟩
+        [ [ idC , (α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ] ∘ (idC +₁ i₁) ∘ f , [ idC , (α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ] ∘ i₂ ∘ h ] ≈⟨ sym ∘[] ⟩
+        [ idC , (α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ] ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ≈⟨ sym #-Fixpoint ⟩
+        α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∎
+        -- refl⟩∘⟨ Terminal.!-unique (coalgebras A) (record { f = coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ; commutes = begin 
+        -- out ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ≈⟨ coit-commutes [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ⟩ 
+        -- (idC +₁ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ≈⟨ ∘[] ⟩ 
+        -- [ (idC +₁ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ (idC +₁ i₁) ∘ f , (idC +₁ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₂ ∘ h ] ≈⟨ []-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘i₂) ⟩ 
+        -- [ (idC ∘ idC +₁ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁) ∘ f , (i₂ ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ h ] ≈⟨ []-cong₂ ((+₁-cong₂ identity² refl) ⟩∘⟨refl) assoc ⟩ 
+        -- [ (idC +₁ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁) ∘ f , i₂ ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ []-cong₂ helper refl ⟩ 
+        -- (α ∘ coit f +₁ (coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ h) ≈⟨ sym (+₁-cong₂ identityˡ refl) ⟩ 
+        -- (idC ∘ α ∘ coit f +₁ (coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ h) ≈⟨ sym +₁∘+₁ ⟩ 
+        -- (idC +₁ (coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])) ∘ (α ∘ coit f +₁ h) ∎ })
+        where 
+          helper'' : α ∘ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁ ≈ α ∘ coit f
+          helper'' = sym-assoc ○ sym (#-Uniformity (sym inject₁))
+          open RMonad (DelayM.kleisli D) using (extend)
+          helper''' : ∀ {X B A} (e : X ⇒ B + X) (g : B ⇒ A) → extend (now ∘ g) ∘ coit e ≈ coit ((g +₁ idC) ∘ e)
+          helper''' {X} {B} {A} e g = sym (Terminal.!-unique (coalgebras A) (record { f = extend (now ∘ g) ∘ coit e ; commutes = begin 
+            out ∘ extend (now ∘ g) ∘ coit e ≈⟨ pullˡ (extendlaw (now ∘ g)) ⟩ 
+            ([ out ∘ now ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ out) ∘ coit e ≈⟨ pullʳ (coit-commutes e) ⟩ 
+            [ out ∘ now ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ (idC +₁ coit e) ∘ e ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩ 
+            (g +₁ extend (now ∘ g)) ∘ (idC +₁ coit e) ∘ e ≈⟨ pullˡ +₁∘+₁ ⟩ 
+            (g ∘ idC +₁ extend (now ∘ g) ∘ coit e) ∘ e ≈⟨ (+₁-cong₂ id-comm (sym identityʳ)) ⟩∘⟨refl ⟩ 
+            ((idC ∘ g +₁ (extend (now ∘ g) ∘ coit e) ∘ idC)) ∘ e ≈⟨ sym (pullˡ +₁∘+₁) ⟩ 
+            (idC +₁ extend (now ∘ g) ∘ coit e) ∘ (g +₁ idC) ∘ e ∎ }))
+          goal₁ : (extend idC ∘ coit (coit f +₁ h)) ∘ i₁ ≈ coit f
+          goal₁ = sym (Terminal.!-unique (coalgebras A) (record { f = (extend idC ∘ coit (coit f +₁ h)) ∘ i₁ ; commutes = begin 
+            out ∘ (extend idC ∘ coit (coit f +₁ h)) ∘ i₁ ≈⟨ pullˡ (pullˡ (extendlaw idC)) ⟩ 
+            (([ out ∘ idC , i₂ ∘ extend idC ] ∘ out) ∘ coit (coit f +₁ h)) ∘ i₁ ≈⟨ (pullʳ (coit-commutes (coit f +₁ h))) ⟩∘⟨refl ⟩ 
+            ([ out ∘ idC , i₂ ∘ extend idC ] ∘ (idC +₁ coit (coit f +₁ h)) ∘ (coit f +₁ h)) ∘ i₁ ≈⟨ (pullˡ []∘+₁) ⟩∘⟨refl ⟩ 
+            ([ (out ∘ idC) ∘ idC , (i₂ ∘ extend idC) ∘ coit (coit f +₁ h) ] ∘ (coit f +₁ h)) ∘ i₁ ≈⟨ pullʳ +₁∘i₁ ⟩ 
+            [ (out ∘ idC) ∘ idC , (i₂ ∘ extend idC) ∘ coit (coit f +₁ h) ] ∘ i₁ ∘ coit f ≈⟨ pullˡ inject₁ ⟩ 
+            ((out ∘ idC) ∘ idC) ∘ coit f ≈⟨ (identityʳ ○ identityʳ) ⟩∘⟨refl ⟩ 
+            out ∘ coit f ≈⟨ coit-commutes f ⟩ 
+            (idC +₁ coit f) ∘ f ≈⟨ {!   !} ⟩ 
+            {!   !} ≈⟨ {!   !} ⟩ 
+            (idC +₁ (extend idC ∘ coit (coit f +₁ h)) ∘ i₁) ∘ f ∎ }))
+          goal₂ : (extend idC ∘ coit (coit f +₁ h)) ∘ i₂ ≈ coit [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h
+          goal₂ = {!   !}
+
+{-
+NOTES:
+From D-module we get:
+1. commute: α ∘ (now ∘ α)* ≈ α ∘ id*
+2. identity: α ∘ now ≈ id
+From Search:
+1. identity₁ : α ∘ now ≈ id
+2. identity² α ∘ later ≈ α
+From Uniform:
+1. Fixpoint: α ∘ coit f ≈ [ idC , α ∘ coit f ] ∘ f
+2. Uniformity: α ∘ coit f ≈ (α ∘ coit g) ∘ h iff g ∘ h ≈ (idC +₁ h) ∘ f
+
+-}
+```

src/Algebra/Search.lagda.md

@@ -21,6 +21,11 @@ module Algebra.Search {o ℓ e} (ambient : Ambient o ℓ e) where
   module _ (D : DelayM) where
     open DelayM D
 
+    record IsSearchAlgebra {A : Obj} (α : F-Algebra-on functor A) : Set (ℓ ⊔ e) where
+      field
+        identity₁ : α ∘ now ≈ idC
+        identity₂ : α ∘ ▷ ≈ α 
+
     record Search-Algebra-on (A : Obj) : Set (ℓ ⊔ e) where
       field
         α : F-Algebra-on functor A
@@ -34,4 +39,8 @@ module Algebra.Search {o ℓ e} (ambient : Ambient o ℓ e) where
         A : Obj
         search-algebra-on : Search-Algebra-on A
       open Search-Algebra-on search-algebra-on public
+
+    IsSearchAlgebra⇒Search-Algebra : ∀ {A} (α : F-Algebra-on functor A) → IsSearchAlgebra α → Search-Algebra
+    IsSearchAlgebra⇒Search-Algebra {A} α is = record { A = A ; search-algebra-on = record { α = α ; identity₁ = identity₁ ; identity₂ = identity₂ } }
+      where open IsSearchAlgebra is
 ```

src/Misc/FreeObject.lagda.md

@@ -0,0 +1,56 @@
+<!--
+```agda
+open import Level
+open import Categories.Category
+open import Categories.Functor
+```
+-->
+
+```agda
+module Misc.FreeObject where
+private
+  variable
+    o ℓ e o' ℓ' e' : Level
+```
+
+# Free objects
+The notion of free object has been formalized in agda-categories:
+
+```agda
+open import Categories.FreeObjects.Free
+``` 
+
+but we need a predicate expressing that an object 'is free':
+
+```agda 
+record IsFreeObject {C : Category o ℓ e} {D : Category o' ℓ' e'} (U : Functor D C) (X : Category.Obj C) (FX : Category.Obj D) : Set (suc (e ⊔ e' ⊔ o ⊔ ℓ ⊔ o' ⊔ ℓ')) where
+
+  private
+    module C = Category C using (Obj; id; identityʳ; identityˡ; _⇒_; _∘_; equiv; module Equiv)
+    module D = Category D using (Obj; _⇒_; _∘_; equiv)
+    module U = Functor U using (₀; ₁)
+
+  field
+     η : C [ X , U.₀ FX ]
+     _* : ∀ {A : D.Obj} → C [ X , U.₀ A ] → D [ FX , A ]
+     *-lift : ∀ {A : D.Obj} (f : C [ X , U.₀ A ]) → C [ (U.₁ (f *) C.∘ η) ≈ f ]
+     *-uniq : ∀ {A : D.Obj} (f : C [ X , U.₀ A ]) (g : D [ FX , A ]) → C [ (U.₁ g) C.∘ η ≈ f ] → D [ g ≈ f * ]
+```
+
+and some way to convert between these notions:
+
+```agda
+IsFreeObject⇒FreeObject : ∀ {C : Category o ℓ e} {D : Category o' ℓ' e'} (U : Functor D C) (X : Category.Obj C) (FX : Category.Obj D) → IsFreeObject U X FX → FreeObject U X
+IsFreeObject⇒FreeObject U X FX isFO = record 
+  { FX = FX 
+  ; η = η 
+  ; _* = _* 
+  ; *-lift = *-lift 
+  ; *-uniq = *-uniq 
+  }
+  where open IsFreeObject isFO
+
+  -- TODO FreeObject⇒IsFreeObject
+
+```
+

src/Monad/Instance/Delay.lagda.md

@@ -88,6 +88,12 @@ Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use the fina
 
         coit-commutes : ∀ (f : Y ⇒ X + Y) → out ∘ (coit f) ≈ (idC +₁ coit f) ∘ f
         coit-commutes f = commutes (! {A = record { A = Y ; α = f }})
+
+        coit-resp-≈ : ∀ {f g : Y ⇒ X + Y} → f ≈ g → coit f ≈ coit g
+        coit-resp-≈ {f} {g} eq = Terminal.!-unique (coalgebras X) (record { f = coit g ; commutes = begin 
+          out ∘ coit g ≈⟨ coit-commutes g ⟩ 
+          (idC +₁ coit g) ∘ g ≈⟨ (refl⟩∘⟨ sym eq) ⟩ 
+          (idC +₁ coit g) ∘ f ∎ })
 ```
 
 Furthermore if we combine the internal algebra structure of Parametrized NNOs with Lambek's lemma, we get the isomorphism `X × N ≅ X + X × N`.

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

@@ -0,0 +1,127 @@
+<!--
+```agda
+open import Level
+open import Categories.Functor
+open import Category.Instance.AmbientCategory using (Ambient)
+open import Categories.Monad
+open import Categories.Monad.Construction.Kleisli
+open import Categories.Monad.Relative renaming (Monad to RMonad)
+open import Data.Product using (_,_; Σ; Σ-syntax)
+open import Categories.Functor.Algebra
+open import Categories.Functor.Coalgebra
+open import Categories.Object.Terminal
+open import Categories.NaturalTransformation.Core
+open import Misc.FreeObject
+```
+-->
+
+```agda
+module Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) where
+  open Ambient ambient
+  open import Categories.Diagram.Coequalizer C 
+  open import Monad.Instance.Delay ambient
+  open import Algebra.Search ambient
+  open import Algebra.ElgotAlgebra ambient
+  open import Algebra.Properties ambient
+  open F-Coalgebra-Morphism using () renaming (f to u; commutes to coalg-commutes)
+  open import Monad.Instance.Delay.Quotienting ambient
+```
+
+# Properties of the quotiented delay monad
+
+```agda
+  module _ (D : DelayM) where
+    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 Monad D-Monad using () renaming (assoc to M-assoc; identityʳ to M-identityʳ)
+    open HomReasoning
+    open M C
+    open MR C
+    open Equiv
+
+    module _ (coeqs : ∀ X → Coequalizer (extend (ι {X})) (D₁ π₁)) where
+      open Quotiented D coeqs
+
+      cond-1 : Set (o ⊔ ℓ ⊔ e)
+      cond-1 = ∀ X → preserves D-Functor (coeqs X)
+
+      -- cond-2' : Set (o ⊔ ℓ ⊔ e)
+      -- cond-2' = ∀ X → Σ[ s-alg-on ∈ Search-Algebra-on D (Ď₀ X) ] is-F-Algebra-Morphism {F = D-Functor} (record { A = D₀ X ; α = μ.η X }) (record { A = Ď₀ X ; α = Search-Algebra-on.α s-alg-on }) (ρ {X})
+      record cond-2' (X : Obj) : Set (o ⊔ ℓ ⊔ e) where
+        field
+          s-alg-on : Search-Algebra-on D (Ď₀ X)
+          ρ-algebra-morphism : is-F-Algebra-Morphism {F = D-Functor} (record { A = D₀ X ; α = μ.η X }) (record { A = Ď₀ X ; α = Search-Algebra-on.α s-alg-on }) (ρ {X})
+      cond-2 = ∀ X → cond-2' X
+
+
+      record cond-3' (X : Obj) : Set (suc o ⊔ suc ℓ ⊔ suc e) where
+        -- Ď₀ X is stable free elgot algebra
+        field
+          elgot : Elgot-Algebra-on (Ď₀ X)
+        elgot-alg = record { A = Ď₀ X ; algebra = elgot }
+
+        open Elgot-Algebra-on elgot
+        field
+          isFO : IsFreeObject elgotForgetfulF X elgot-alg
+        freeobject = IsFreeObject⇒FreeObject elgotForgetfulF X elgot-alg isFO
+        field
+          isStable : IsStableFreeElgotAlgebra freeobject
+
+        -- ρ is D-algebra morphism
+        field
+          ρ-algebra-morphism : is-F-Algebra-Morphism {F = D-Functor} (record { A = D₀ X ; α = μ.η X }) (record { A = Ď₀ X ; α = out # }) (ρ {X})
+          ρ-law : ρ ≈ ((ρ ∘ now +₁ idC) ∘ out) #
+      cond-3 = ∀ X → cond-3' X
+
+      record cond-4 : Set (o ⊔ ℓ ⊔ e) where
+
+      2⇒3 : cond-2 → cond-3
+      2⇒3 c-2 X = record
+        { elgot = {!   !} 
+        ; isFO = {!   !}
+        ; isStable = {!   !}
+        ; ρ-algebra-morphism = {!   !}
+        ; ρ-law = {!   !}
+        }
+
+      1⇒2 : cond-1 → cond-2
+      1⇒2 c-1 X = record { s-alg-on = s-alg-on ; ρ-algebra-morphism = 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)
+          s-alg-on : Search-Algebra-on D (Ď₀ X)
+          s-alg-on = record 
+            { α = α'
+            ; identity₁ = ρ-epi (α' ∘ now) idC (begin 
+              (α' ∘ now) ∘ ρ ≈⟨ pullʳ (η.commute ρ) ⟩ 
+              α' ∘ D₁ ρ ∘ now ≈⟨ pullˡ (sym D-universal) ⟩
+              (ρ ∘ μ.η X) ∘ now ≈⟨ cancelʳ M-identityʳ ⟩
+              ρ ≈⟨ sym identityˡ ⟩
+              idC ∘ ρ ∎) 
+            ; identity₂ = IsCoequalizer⇒Epi (c-1 X) (α' ∘ ▷) α' (begin 
+              (α' ∘ ▷) ∘ 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
+              μ∘Dι : μ.η X ∘ D₁ ι ≈ extend ι
+              μ∘Dι = sym k-assoc ○ extend-≈ (cancelˡ k-identityʳ)
+              eq₁ : D₁ (extend ι) ≈ D₁ (μ.η X) ∘ D₁ (D₁ ι)
+              eq₁ = sym (begin 
+                D₁ (μ.η X) ∘ D₁ (D₁ ι) ≈⟨ sym D-homomorphism ⟩ 
+                D₁ (μ.η X ∘ D₁ ι) ≈⟨ D-resp-≈ μ∘Dι ⟩
+                D₁ (extend ι) ∎)
+              α' = D-coequalize {h = ρ {X} ∘ μ.η X} (begin 
+                (ρ ∘ μ.η X) ∘ D₁ (extend ι) ≈⟨ (refl⟩∘⟨ eq₁) ⟩ 
+                (ρ ∘ μ.η X) ∘ D₁ (μ.η X) ∘ D₁ (D₁ ι) ≈⟨ pullʳ (pullˡ M-assoc) ⟩
+                ρ ∘ (μ.η X ∘ μ.η (D₀ X)) ∘ D₁ (D₁ ι) ≈⟨ (refl⟩∘⟨ pullʳ (μ.commute ι)) ⟩
+                ρ ∘ μ.η X ∘ (D₁ ι) ∘ μ.η (X × N) ≈⟨ (refl⟩∘⟨ pullˡ μ∘Dι) ⟩
+                ρ ∘ extend ι ∘ μ.η (X × N) ≈⟨ pullˡ equality ⟩
+                (ρ ∘ D₁ π₁) ∘ μ.η (X × N) ≈⟨ (pullʳ (sym (μ.commute π₁)) ○ sym-assoc) ⟩
+                (ρ ∘ μ.η X) ∘ D₁ (D₁ π₁) ∎)
+```

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

@@ -13,6 +13,7 @@ open import Categories.Functor.Algebra
 open import Categories.Functor.Coalgebra
 open import Categories.Object.Terminal
 open import Categories.NaturalTransformation.Core
+open import Misc.FreeObject
 ```
 -->
 
@@ -22,6 +23,8 @@ module Monad.Instance.Delay.Quotienting {o ℓ e} (ambient : Ambient o ℓ e) wh
   open import Categories.Diagram.Coequalizer C 
   open import Monad.Instance.Delay ambient
   open import Algebra.Search ambient
+  open import Algebra.ElgotAlgebra ambient
+  open import Algebra.Properties ambient
   open F-Coalgebra-Morphism using () renaming (f to u; commutes to coalg-commutes)
 ```
 
@@ -64,7 +67,7 @@ We will now show that the following conditions are equivalent:
     open MR C
     open Equiv
 
-    module _ (coeqs : ∀ X → Coequalizer (extend (ι {X})) (D₁ π₁)) where
+    module Quotiented (coeqs : ∀ X → Coequalizer (extend (ι {X})) (D₁ π₁)) where
 
       Ď₀ : Obj → Obj
       Ď₀ X = Coequalizer.obj (coeqs X)
@@ -188,55 +191,4 @@ We will now show that the following conditions are equivalent:
         { η = λ X → ρ {X} 
         ; commute = λ {X} {Y} f → Coequalizer.universal (coeqs X)
         })
-
+```
-      cond-1 : Set (o ⊔ ℓ ⊔ e)
-      cond-1 = ∀ X → preserves D-Functor (coeqs X)
-
-      cond-2 : Set (o ⊔ ℓ ⊔ e)
-      cond-2 = ∀ X → Σ[ s-alg-on ∈ Search-Algebra-on D (Ď₀ X) ] is-F-Algebra-Morphism {F = D-Functor} (record { A = D₀ X ; α = μ.η X }) (record { A = Ď₀ X ; α = Search-Algebra-on.α s-alg-on }) (ρ {X})
-
-      cond-3 : Set (o ⊔ ℓ ⊔ e)
-      cond-3 = {!   !} 
-
-      cond-4 : Set (o ⊔ ℓ ⊔ e)
-      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₁ ρ ∎)
-        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)
-          s-alg-on : Search-Algebra-on D (Ď₀ X)
-          s-alg-on = record 
-            { α = α'
-            ; identity₁ = ρ-epi (α' ∘ now) idC (begin 
-              (α' ∘ now) ∘ ρ ≈⟨ pullʳ (η.commute ρ) ⟩ 
-              α' ∘ D₁ ρ ∘ now ≈⟨ pullˡ (sym D-universal) ⟩
-              (ρ ∘ μ.η X) ∘ now ≈⟨ cancelʳ M-identityʳ ⟩
-              ρ ≈⟨ sym identityˡ ⟩
-              idC ∘ ρ ∎) 
-            ; identity₂ = IsCoequalizer⇒Epi (c-1 X) (α' ∘ ▷) α' (begin 
-              (α' ∘ ▷) ∘ 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
-              μ∘Dι : μ.η X ∘ D₁ ι ≈ extend ι
-              μ∘Dι = sym k-assoc ○ extend-≈ (cancelˡ k-identityʳ)
-              eq₁ : D₁ (extend ι) ≈ D₁ (μ.η X) ∘ D₁ (D₁ ι)
-              eq₁ = sym (begin 
-                D₁ (μ.η X) ∘ D₁ (D₁ ι) ≈⟨ sym D-homomorphism ⟩ 
-                D₁ (μ.η X ∘ D₁ ι) ≈⟨ D-resp-≈ μ∘Dι ⟩
-                D₁ (extend ι) ∎)
-              α' = D-coequalize {h = ρ {X} ∘ μ.η X} (begin 
-                (ρ ∘ μ.η X) ∘ D₁ (extend ι) ≈⟨ (refl⟩∘⟨ eq₁) ⟩ 
-                (ρ ∘ μ.η X) ∘ D₁ (μ.η X) ∘ D₁ (D₁ ι) ≈⟨ pullʳ (pullˡ M-assoc) ⟩
-                ρ ∘ (μ.η X ∘ μ.η (D₀ X)) ∘ D₁ (D₁ ι) ≈⟨ (refl⟩∘⟨ pullʳ (μ.commute ι)) ⟩
-                ρ ∘ μ.η X ∘ (D₁ ι) ∘ μ.η (X × N) ≈⟨ (refl⟩∘⟨ pullˡ μ∘Dι) ⟩
-                ρ ∘ extend ι ∘ μ.η (X × N) ≈⟨ pullˡ equality ⟩
-                (ρ ∘ D₁ π₁) ∘ μ.η (X × N) ≈⟨ (pullʳ (sym (μ.commute π₁)) ○ sym-assoc) ⟩
-                (ρ ∘ μ.η X) ∘ D₁ (D₁ π₁) ∎)
-```

src/Monad/Instance/K.lagda.md

@@ -11,6 +11,7 @@ open import Categories.Monad
 open import Categories.Monad.Strong
 open import Category.Instance.AmbientCategory using (Ambient)
 open import Categories.NaturalTransformation
+open import Categories.Object.Terminal
 -- open import Data.Product using (_,_; Σ; Σ-syntax)
 ```
 -->
@@ -37,6 +38,7 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
   open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
 
   open Equiv
+  open HomReasoning
 
 ```
 
@@ -55,9 +57,6 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
 
     K : Monad C
     K = adjoint⇒monad adjoint
-
-    -- EilenbergMoore⇒UniformIterationAlgebras : StrongEquivalence (EilenbergMoore K) (Uniform-Iteration-Algebras D)
-    -- EilenbergMoore⇒UniformIterationAlgebras = {!   !}
 ```
 
 ### *Proposition 19* If the algebras are stable then K is strong
@@ -78,11 +77,18 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
     KStrong = record 
       { M = K 
       ; strength = record
-        { strengthen = ntHelper (record { η = τ ; commute = λ f → {!   !} }) 
+        { strengthen = ntHelper (record { η = τ ; commute = commute' }) 
-        ; identityˡ = {!   !}
+        ; identityˡ = λ {X} → begin 
-        ; η-comm = {!   !}
+          K₁ π₂ ∘ τ _ ≈⟨ refl ⟩
-        ; μ-η-comm = {!   !}
+          Uniform-Iteration-Algebra-Morphism.h ((algebras (Terminal.⊤ terminal × X) FreeObject.*) (FreeObject.η (algebras X) ∘ π₂)) ∘ τ _ ≈⟨ {!   !} ⟩
-        ; strength-assoc = {!   !}
+          {!   !} ≈⟨ {!   !} ⟩
+          {!   !} ≈⟨ {!   !} ⟩
+          π₂ ∎
+        ; η-comm = λ {A} {B} → begin τ _ ∘ (idC ⁂ η (A , B) B) ≈⟨ τ-η (A , B) ⟩ η (A , B) (A × B) ∎
+        ; μ-η-comm = λ {A} {B} → {!   !}
+        ; strength-assoc = λ {A} {B} {D} → begin 
+          K₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ τ _ ≈⟨ {!   !} ⟩ 
+          τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎
         }
       }
       where
@@ -107,4 +113,12 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
 
         τ-comm : ∀ {X Y Z : Obj} (h : Z ⇒ K₀ Y + Z) → τ (X , Y) ∘ (idC ⁂ [ FreeObject.FX (algebras Y) , h ]#) ≈ [ FreeObject.FX (algebras (X × Y)) , (τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ]#
         τ-comm {X} {Y} {Z} h = ♯-preserving (stable Y) (η (X , Y) (X × Y)) h
+
+        commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂) 
+          → τ P₂ ∘ ((fst fg) ⁂ K₁ (snd fg)) ≈ K₁ ((fst fg) ⁂ (snd fg)) ∘ τ P₁
+        commute' {(U , V)} {(W , X)} (f , g) = begin 
+          τ _ ∘ (f ⁂ Uniform-Iteration-Algebra-Morphism.h ((algebras V FreeObject.*) (FreeObject.η (algebras X) ∘ g))) ≈⟨ {!   !} ⟩ 
+          {!   !} ≈⟨ {!   !} ⟩
+          {!   !} ≈⟨ {!   !} ⟩
+          Uniform-Iteration-Algebra-Morphism.h ((algebras (U × V) FreeObject.*) (FreeObject.η (algebras (W × X)) ∘ (f ⁂ g))) ∘ τ _ ∎
 ```