From 0165423fcf553cd8e0075a788f9b9dfccedec944 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Tue, 3 Oct 2023 19:44:08 +0200
Subject: [PATCH] =?UTF-8?q?=F0=9F=9A=A7=20Started=20working=20on=20quotien?=
 =?UTF-8?q?ting=20the=20delay=20monad?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Makefile                                      |  3 +
 src/Monad/Instance/Delay.lagda.md             |  4 +-
 src/Monad/Instance/Delay/Quotienting.lagda.md | 58 +++++++++++++++++--
 3 files changed, 56 insertions(+), 9 deletions(-)

diff --git a/Makefile b/Makefile
index 355ac99..d52d115 100644
--- a/Makefile
+++ b/Makefile
@@ -31,3 +31,6 @@ push':
 
 Everything.agda:
 	git ls-tree --full-tree -r --name-only HEAD | egrep '^src/[^\.]*.l?agda(\.md)?' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort > Everything.agda
+
+open:
+	firefox public/index.html
\ No newline at end of file
diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md
index 6019898..2cf1bf4 100644
--- a/src/Monad/Instance/Delay.lagda.md
+++ b/src/Monad/Instance/Delay.lagda.md
@@ -1,6 +1,5 @@
 <!--
 ```agda
-{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Categories.Category
 open import Categories.Monad
@@ -22,8 +21,6 @@ module Monad.Instance.Delay {o ℓ e} (ambient : Ambient o ℓ e) where
   open Ambient ambient
 ```
 
--- TODO SERGEYS LÖSUNG: https://q.uiver.app/#q=WzAsNyxbMCwwLCJYXFx0aW1lcyBERFkiXSxbMiwwLCJEKFhcXHRpbWVzIERZKSJdLFs0LDAsIkREKFhcXHRpbWVzIFkpIl0sWzAsMiwiWFxcdGltZXMgKERZK0REWSkiXSxbMiwyLCJYXFx0aW1lcyBEWSsgWFxcdGltZXMgRERZIl0sWzQsMiwiWFxcdGltZXMgWSsgREQoWFxcdGltZXMgWSkiXSxbMCw0LCJYXFx0aW1lcyBZKyBYXFx0aW1lcyBERFkiXSxbMCwzLCJpZFxcdGltZXMgb3V0IiwyXSxbMCwxLCJcXHRhdSJdLFsxLDIsIlxcdGF1XioiXSxbMyw0LCIoaWQrXFx0YXUpZGlzdCJdLFs0LDUsIltvdXRcXHRhdSxpbnJcXHRhdV4qXSJdLFsyLDUsIm91dCJdLFsxLDRdLFs2LDUsImlkK1xcdGF1XipcXHRhdSIsMl0sWzMsNiwiWyhpZCArIGlkXFx0aW1lcyBub3cpZGlzdCAoaWRcXHRpbWVzIG91dCksaW5yXWRpc3QiLDJdXQ==
-
 ## Definition
 
 The delay monad is usually defined as a coinductive type with two constructors `now : X → D X` and `later : D X → D X`, e.g. in the [agda-stdlib](https://agda.github.io/agda-stdlib/Effect.Monad.Partiality.html#1523)
@@ -418,6 +415,7 @@ Next we will show that the delay monad is strong, by giving a natural transforma
               (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩ 
             τ _ ∘ (idC ⁂ extend idC) ∎
             where
+              -- diagram: https://q.uiver.app/#q=WzAsNyxbMCwwLCJYXFx0aW1lcyBERFkiXSxbMiwwLCJEKFhcXHRpbWVzIERZKSJdLFs0LDAsIkREKFhcXHRpbWVzIFkpIl0sWzAsMiwiWFxcdGltZXMgKERZK0REWSkiXSxbMiwyLCJYXFx0aW1lcyBEWSsgWFxcdGltZXMgRERZIl0sWzQsMiwiWFxcdGltZXMgWSsgREQoWFxcdGltZXMgWSkiXSxbMCw0LCJYXFx0aW1lcyBZKyBYXFx0aW1lcyBERFkiXSxbMCwzLCJpZFxcdGltZXMgb3V0IiwyXSxbMCwxLCJcXHRhdSJdLFsxLDIsIlxcdGF1XioiXSxbMyw0LCIoaWQrXFx0YXUpZGlzdCJdLFs0LDUsIltvdXRcXHRhdSxpbnJcXHRhdV4qXSJdLFsyLDUsIm91dCJdLFsxLDRdLFs2LDUsImlkK1xcdGF1XipcXHRhdSIsMl0sWzMsNiwiWyhpZCArIGlkXFx0aW1lcyBub3cpZGlzdCAoaWRcXHRpbWVzIG91dCksaW5yXWRpc3QiLDJdXQ==
               square : out ∘ extend (τ (X , Y)) ∘ τ _ ≈ [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
               square = begin 
                 out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ pullˡ (extendlaw (τ (X , Y))) ⟩ 
diff --git a/src/Monad/Instance/Delay/Quotienting.lagda.md b/src/Monad/Instance/Delay/Quotienting.lagda.md
index 5c21293..8c9c5dd 100644
--- a/src/Monad/Instance/Delay/Quotienting.lagda.md
+++ b/src/Monad/Instance/Delay/Quotienting.lagda.md
@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 
 open import Categories.Functor
@@ -12,16 +13,61 @@ open import Categories.Monad.Relative renaming (Monad to RMonad)
 ```agda
 module Monad.Instance.Delay.Quotienting {o ℓ e} (ambient : Ambient o ℓ e) where
   open Ambient ambient
-
   open import Categories.Diagram.Coequalizer C 
   open import Monad.Instance.Delay ambient
+```
 
+
+# Quotienting the delay monad by weak bisimilarity
+
+The coinductive definition of the delay monad yields a 'wrong' kind of equality called *strong bisimilarity*, which differentiates between computations with different execution times, instead we want two computations to be equal, when they both terminate with the same result (or don't terminate at all).
+This is called *weak bisimilarity*. The ideas is then to quotient the delay monad with this 'right' kind of equality and show that the result $\tilde{D}$ is again a (strong) monad.
+
+In category theory existence of **coequalizers** corresponds to qoutienting, so we will express the quotiented delay monad via the following coequalizer:
+
+<!-- https://q.uiver.app/#q=WzAsMyxbMCwwLCJEKFggXFx0aW1lcyBcXG1hdGhiYntOfSkiXSxbMiwwLCJEWCJdLFs0LDAsIlxcdGlsZGV7RH1YIl0sWzEsMiwiXFxyaG9fWCJdLFswLDEsIkQgXFxwaV8xIiwyLHsib2Zmc2V0IjoxfV0sWzAsMSwiXFxpb3RhXioiLDAseyJvZmZzZXQiOi0xfV1d -->
+<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsMyxbMCwwLCJEKFggXFx0aW1lcyBcXG1hdGhiYntOfSkiXSxbMiwwLCJEWCJdLFs0LDAsIlxcdGlsZGV7RH1YIl0sWzEsMiwiXFxyaG9fWCJdLFswLDEsIkQgXFxwaV8xIiwyLHsib2Zmc2V0IjoxfV0sWzAsMSwiXFxpb3RhXioiLDAseyJvZmZzZXQiOi0xfV1d&embed" width="765" height="176" style="border-radius: 8px; border: none;"></iframe>
+
+## Preliminaries
+
+Existence of the coequalizer doesn't suffice, we will need some conditions having to do with preservation of the coequalizer, so let's first define what it means for a coequalizer to be preserved by an endofunctor:
+
+```agda
+  preserves : ∀ {X Y} {f g : X ⇒ Y} → Endofunctor C → Coequalizer f g → Set (o ⊔ ℓ ⊔ e)
+  preserves {X} {Y} {f} {g} F coeq = Coequalizer (Functor.₁ F f) (Functor.₁ F g)
+```
+
+We will now show that the following conditions are equivalent:
+
+1. For every $X$, the coequalizer is preserved by $D$
+2. every $\tilde{D}X$ extends to a search-algebra, so that each $ρ_X$ is a D-algebra morphism
+3. for every $X$, $(\tilde{D}X, ρ ∘ now : X → \tilde{D}X)$ is a stable free elgot algebra on X, $ρ_X$ is a D-algebra morphism and $ρ_X = ((ρ_X ∘ now + id) ∘ out)^\#$
+4. $\tilde{D}$ extends to a strong monad, so that $ρ$ is a strong monad morphism
+
+```agda
   module _ (D : DelayM) where
-    open DelayM D
+    open DelayM D renaming (functor to D-Fun; monad to D-Monad; kleisli to D-Kleisli)
 
-    open Functor functor using () renaming (F₁ to D₁)
-    open RMonad kleisli
+    open Functor D-Fun using () renaming (F₁ to D₁)
+    open RMonad D-Kleisli
 
-    module _ {X : Obj} (coeq : Coequalizer (extend (ι {X})) (D₁ π₁)) where
-      -- TODO
+
+    
+
+    module _ (coeqs : ∀ X → Coequalizer (extend (ι {X})) (D₁ π₁)) where
+
+      Ď₀ : Obj → Obj
+      Ď₀ X = Coequalizer.obj (coeqs X)
+
+      cond-1 : Set (o ⊔ ℓ ⊔ e)
+      cond-1 = ∀ {X} → preserves D-Fun (coeqs X)
+
+      cond-2 : Set (o ⊔ ℓ ⊔ e)
+      cond-2 = {!   !}
+
+      cond-3 : Set (o ⊔ ℓ ⊔ e)
+      cond-3 = {!   !}
+
+      cond-4 : Set (o ⊔ ℓ ⊔ e)
+      cond-4 = {!   !}
 ```
\ No newline at end of file