✨ Added index with some nice text

Makefile

@@ -9,10 +9,9 @@ pandoc: public/*.md
 	)
 
 agda: Everything.agda
-	agda --html --html-dir=public Everything.agda --html-highlight=auto -i.
+	agda --html --html-dir=public index.lagda.md --html-highlight=auto -i.
 	rm -f public/Agda.css
 	cp Agda.css public/Agda.css
-	mv public/Everything.html public/index.html
 
 clean:
 	rm -f  Everything.agda

index.lagda.md

@@ -0,0 +1,52 @@
+# Implementing Categorical Notions of Partiality and Delay in Agda
+
+To see a full list of all the modules go to:
+
+```agda
+open import Everything
+```
+
+For my bachelor's thesis I am implementing categorical notions of partiality in agda using the *agda-categories* library. The repo for this project can be found [here](https://git8.cs.fau.de/theses/bsc-leon-vatthauer).
+This mostly is an implementation of this paper by Sergey Goncharov: [arxiv](https://arxiv.org/abs/2102.11828)
+
+## Structure
+
+We start out by formalizing Caprettas Delay Monad in category theory by existence of final coalgebras and showing that it is strong.
+
+```agda
+open import Monad.Instance.Delay
+```
+
+The next step is to quotient the delay monad by weak bisimilarity, in category theory this corresponds to existence of fitting coequalizers.
+This quotiented structure is not directly monadic, we implement conditions under which it extends to a monad and prove it.
+
+```agda
+open import Monad.Instance.Delay.Quotienting
+```
+
+Next come some basic definitions of iteration algebras, we differentiate between uniform-iteration algebras and (un-)guarded elgot algebras:
+
+```agda
+open import Algebra.ElgotAlgebra
+open import Category.Construction.ElgotAlgebras
+open import Algebra.UniformIterationAlgebra
+open import Category.Construction.UniformIterationAlgebras
+```
+
+Existence of free uniform-iteration algebras yields a monad that is of interest to us, we call it **K** and want to show some of it's properties (i.e. that it is strong and an equational lifting monad):
+
+```agda
+open import Monad.Instance.K -- TODO move to Monad.Construction.K
+```
+
+Later we will also show that free uniform-iteration algebras coincide with free elgot algebras
+
+```agda
+-- TODO
+```
+
+For the final step we will come back to the quotiented delay monad and show that under variations of the axiom of countable choice it is an explicit construction for the aforementioned monad **K**.
+
+```agda
+open import Monad.Instance.Delay.Properties
+```

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,128 @@
+<!--
+```agda
+{-# OPTIONS --allow-unsolved-metas #-}
+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

@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Categories.FreeObjects.Free
 open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_)
@@ -11,6 +12,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 +39,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 +58,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 +78,18 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
     KStrong = record 
       { M = K 
       ; strength = record
-        { strengthen = ntHelper (record { η = τ ; commute = λ f → {!   !} }) 
-        ; identityˡ = {!   !}
-        ; η-comm = {!   !}
-        ; μ-η-comm = {!   !}
-        ; strength-assoc = {!   !}
+        { strengthen = ntHelper (record { η = τ ; commute = commute' }) 
+        ; identityˡ = λ {X} → begin 
+          K₁ π₂ ∘ τ _ ≈⟨ refl ⟩
+          Uniform-Iteration-Algebra-Morphism.h ((algebras (Terminal.⊤ terminal × X) FreeObject.*) (FreeObject.η (algebras X) ∘ π₂)) ∘ τ _ ≈⟨ {!   !} ⟩
+          {!   !} ≈⟨ {!   !} ⟩
+          {!   !} ≈⟨ {!   !} ⟩
+          π₂ ∎
+        ; η-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 +114,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))) ∘ τ _ ∎
 ```