🔀 Merge branch 'main' of git8.cs.fau.de:theses/bsc-leon-vatthauer

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

README.md

@@ -16,11 +16,11 @@ So far the contributions are:
     - `Categories.Category.Distributive`
     - `Categories.Category.Extensive.Bundle`
     - `Categories.Category.Extensive.Properties.Distributive`
-3. Parametrized (or stable) natural numbers objects [[WIP](https://github.com/agda/agda-categories/pull/394)]
+3. Parametrized (or stable) natural numbers objects [[merged](https://github.com/agda/agda-categories/pull/394)]
     - `Categories.Object.NaturalNumbers.Parametrized`
     - `Categories.Object.NaturalNumbers.Properties.F-Algebra`
     - `Categories.Object.NaturalNumbers.Properties.Parametrized`
-4. Commutative categories [TODO]
+4. Commutative monad [TODO]
 
 ## TODO
 TODOs are found inside the literate agda files!

src/Category/Instance/AmbientCategory.lagda.md

@@ -83,4 +83,23 @@ module Category.Instance.AmbientCategory where
         open MR C
         open HomReasoning
         open Equiv
+  
+    iso-epi-from : ∀ {X Y} → (iso : X ≅ Y) → Epi (_≅_.from iso)
+    iso-epi-from iso = λ f g eq → begin 
+      f ≈⟨ introʳ (_≅_.isoʳ iso) ⟩ 
+      (f ∘ M'._≅_.from iso ∘ M'._≅_.to iso) ≈⟨ pullˡ eq ⟩
+      ((g ∘ M'._≅_.from iso) ∘ M'._≅_.to iso) ≈⟨ cancelʳ (_≅_.isoʳ iso) ⟩
+      g ∎
+      where 
+        open HomReasoning
+        open MR C
+    iso-epi-to : ∀ {X Y} → (iso : X ≅ Y) → Epi (_≅_.to iso)
+    iso-epi-to iso = λ f g eq → begin 
+      f ≈⟨ introʳ (_≅_.isoˡ iso) ⟩ 
+      (f ∘ M'._≅_.to iso ∘ M'._≅_.from iso) ≈⟨ pullˡ eq ⟩
+      ((g ∘ M'._≅_.to iso) ∘ M'._≅_.from iso) ≈⟨ cancelʳ (_≅_.isoˡ iso) ⟩
+      g ∎
+      where 
+        open HomReasoning
+        open MR C
 ```

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
@@ -72,7 +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-≅)
-
 ```
 
 Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use the final coalgebras to get a *coiteration operator* `coit`:
@@ -100,7 +98,6 @@ At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `(Y
 
       ι : X × N ⇒ DX
       ι = u (! {A = record { A = X × N ; α = _≅_.from nno-iso }})
-
 ```
 
 ## Delay is a monad
@@ -294,7 +291,7 @@ Next we will show that the delay monad is strong, by giving a natural transforma
       open import Categories.Category.Monoidal.Core
       open Monoidal monoidal
       open import Categories.Monad.Relative using () renaming (Monad to RMonad)
-      open RMonad kleisli using (extend) renaming (assoc to k-assoc)
+      open RMonad kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
       open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_)
       open Monad monad using () renaming (η to η'; μ to μ')
       module η = NaturalTransformation η'
@@ -346,6 +343,15 @@ Next we will show that the delay monad is strong, by giving a natural transforma
               out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ (idC ⁂ out⁻¹) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimʳ (⁂∘⁂ ○ (⁂-cong₂ identity² (_≅_.isoʳ out-≅)) ○ ((⟨⟩-cong₂ identityˡ identityˡ) ○ ⁂-η)))) ⟩
               out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∎
 
+            τ-now : τ ∘ (idC ⁂ now) ≈ now
+            τ-now = begin 
+              τ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ (⁂-cong₂ identity² refl)) ⟩ 
+              τ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullˡ τ-helper ⟩
+              (out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullʳ (pullʳ dstr-law₁) ⟩
+              out⁻¹ ∘ (idC +₁ τ) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩
+              out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
+              now ∎
+
             τ-unique : (t : X × D₀ Y ⇒ D₀ (X × Y)) → (out ∘ t ≈ (idC +₁ t) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) → t ≈ τ
             τ-unique t t-commutes = sym (!-unique (record { f = t ; commutes = t-commutes }))
 
@@ -388,52 +394,71 @@ Next we will show that the delay monad is strong, by giving a natural transforma
                 π₂ ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ pullˡ ∘[] ⟩
                 [ π₂ ∘ ((idC ⁂ i₁)) , π₂ ∘ (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ π₂∘⁂ π₂∘⁂) ⟩∘⟨refl ⟩
                 (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∎)
+
           μ-η-comm' : ∀ {X Y} → extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈ τ (X , Y) ∘ (idC ⁂ extend idC)
           μ-η-comm' {X} {Y} = begin 
             extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y)) (record { f = extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ; commutes = begin 
-              out ∘ extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _ ≈⟨ pullˡ (extendlaw idC) ⟩ 
-              ([ out ∘ idC , i₂ ∘ extend idC ] ∘ out) ∘ extend (now ∘ τ (X , Y)) ∘ τ _ ≈⟨ pullʳ (pullˡ (extendlaw (now ∘ τ (X , Y)))) ⟩ 
-              [ out ∘ idC , i₂ ∘ extend idC ] ∘ ([ out ∘ now ∘ τ _ , i₂ ∘ extend (now ∘ τ _) ] ∘ out) ∘ τ _ ≈⟨ refl⟩∘⟨ (pullʳ (τ-law _)) ⟩ 
-              [ out ∘ idC , i₂ ∘ extend idC ] ∘ [ out ∘ now ∘ τ _ , i₂ ∘ extend (now ∘ τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (sym []∘+₁) ⟩∘⟨ (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl) ⟩ 
-              ([ out , i₂ ] ∘ (idC +₁ extend idC)) ∘ (τ _ +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩
-              {!   !} ≈⟨ {!   !} ⟩ 
-              -- TODO only works if (now +₁ now) ∘ out ≈ out ∘ now
-              {!   !} ≈⟨ {!   !} ⟩ 
-              [ out , i₂ ] ∘ (idC +₁ extend idC) ∘ (τ _ +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (now +₁ idC) ∘ (idC +₁ now) ∘ out , (now +₁ idC) ∘ i₂ ]) ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩ 
-              [ out , i₂ ] ∘ (idC +₁ extend idC) ∘ (τ _ +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (now +₁ idC) ∘ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩ 
-              [ out , i₂ ] ∘ (idC +₁ extend idC) ∘ (τ _ +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (now +₁ idC)) ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩ 
-              [ out , i₂ ] ∘ (idC +₁ extend idC) ∘ (τ _ +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ ((idC ⁂ now) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩ 
-              [ out ∘ (τ _ ∘ (idC ⁂ now)) , i₂ ] ∘ (idC +₁ extend idC) ∘ (idC +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩ 
-              [ out ∘ now , i₂ ] ∘ (idC +₁ extend idC) ∘ (idC +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩ 
-              (idC +₁ extend idC) ∘ (idC +₁ extend (now ∘ τ _)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩ 
-              (idC +₁ (extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) ∎ })) ⟩ 
-            u (Terminal.! (coalgebras (X × Y)) {A = record { A = X × D₀ (D₀ Y) ; α = distributeˡ⁻¹ ∘ (idC ⁂ [ (idC +₁ now) ∘ out , i₂ ]) ∘ (idC ⁂ out) }}) ≈⟨ {!   !} ⟩ 
+              out ∘ extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _ ≈⟨ refl⟩∘⟨ (pullˡ id*∘Dτ) ⟩
+              out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ square ⟩
+              [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ sym-assoc ○ (assoc ○ tri) ⟩∘⟨refl ⟩
+              ((idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩
+              (idC +₁ (extend (τ _) ∘ τ _)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ refl (sym (pullˡ id*∘Dτ))) ⟩∘⟨refl ⟩
+              (idC +₁ (extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩
+            u (Terminal.! (coalgebras (X × Y)) {A = record { A = X × D₀ (D₀ Y) ; α = [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }}) ≈⟨ Terminal.!-unique (coalgebras (X × Y)) (record { f = τ _ ∘ (idC ⁂ extend idC) ; commutes = begin 
+              out ∘ τ _ ∘ (idC ⁂ extend idC) ≈⟨ pullˡ (τ-law (X , Y)) ⟩ 
+              ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ extend idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩
+              (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out ∘ extend idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (extendlaw idC) ⟩
+              (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out ∘ idC , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (([]-cong₂ identityʳ refl) ⟩∘⟨refl) ⟩
+              (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩
+              (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ pullˡ (assoc ○ tri₂) ⟩
+              ((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩
+              (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩ 
             τ _ ∘ (idC ⁂ extend idC) ∎
             where
-              β : ∀ {A} → D₀ A + D₀ (D₀ A) ⇒ A + D₀ (D₀ A)
-              β {A} = [ ((idC +₁ now) ∘ out) , i₂ ]
-              β⁻¹ : ∀ {A} → A + D₀ (D₀ A) ⇒ D₀ A + D₀ (D₀ A)
-              β⁻¹ {A} = [ (i₁ ∘ now) , i₂ ]
-              β∘β⁻¹ : ∀ {A} → β {A} ∘ β⁻¹ ≈ idC
-              β∘β⁻¹ = begin 
-                [ ((idC +₁ now) ∘ out) , i₂ ] ∘ [ (i₁ ∘ now) , i₂ ] ≈⟨ ∘[] ⟩ 
-                [ [ ((idC +₁ now) ∘ out) , i₂ ] ∘ (i₁ ∘ now) , [ ((idC +₁ now) ∘ out) , i₂ ] ∘ i₂ ] ≈⟨ []-cong₂ (pullˡ inject₁) inject₂ ⟩
-                [ ((idC +₁ now) ∘ out) ∘ now , i₂ ] ≈⟨ []-cong₂ (pullʳ unitlaw) refl ⟩
-                [ (idC +₁ now) ∘ i₁ , i₂ ] ≈⟨ []-cong₂ (+₁∘i₁ ○ identityʳ) refl ⟩
-                [ i₁ , i₂ ] ≈⟨ +-η ⟩
-                idC ∎
-              -- diag₁ : ((idC ⁂ now) +₁ τ _) ∘ distributeˡ⁻¹ {X} {Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈ out ∘ τ _
-              -- diag₁ = begin 
-              --   ((idC ⁂ now) +₁ τ _) ∘ distributeˡ⁻¹ {X} {Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
-              --   (idC +₁ τ _) ∘ ((idC ⁂ now) +₁ idC) ∘ distributeˡ⁻¹ {X} {Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
-              --   (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ((idC ⁂ (now +₁ idC))) ∘ ( idC ⁂ [ (idC +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
-              --   (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (now +₁ idC) ∘ (idC +₁ now) ∘ out , (now +₁ idC) ∘ i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
-              --   (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ (now +₁ now) ∘ out , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
-              --   (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ [ out ∘ now , i₂ ] ∘ out) ≈⟨ {!   !} ⟩ 
-              --   (idC +₁ τ _) ∘ distributeˡ⁻¹ {X} {D₀ Y} {D₀ (D₀ Y)} ∘ ( idC ⁂ out) ≈⟨ sym (τ-law (X , A (Terminal.⊤ (coalgebras Y)))) ⟩ 
-              --   out ∘ τ _ ∎
-              diag₂ = τ-law
-              diag₃ = out-law {Y = D₀ (X × Y)} (extend idC)
+              -- 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))) ⟩ 
+                ([ out ∘ τ (X , Y) , i₂ ∘ extend (τ (X , Y)) ] ∘ out) ∘ τ _ ≈⟨ pullʳ (τ-law _) ⟩ 
+                [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎
+              tri : [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈ (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹
+              tri = begin 
+                [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈⟨ pullˡ []∘+₁ ⟩ 
+                [ (out ∘ τ _) ∘ idC , (i₂ ∘ extend (τ (X , Y))) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ (identityʳ ○ τ-law (X , Y)) assoc) ⟩∘⟨refl ⟩ 
+                [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ (X , Y)) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ refl k-identityʳ) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ 
+                [ (idC +₁ extend (τ _) ∘ now) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ identity² (pullʳ (τ-now (X , D₀ Y)))) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩ 
+                [ (idC ∘ idC +₁ (extend (τ _) ∘ τ _) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ (pullˡ +₁∘+₁) +₁∘i₂) ⟩∘⟨refl) ⟩ 
+                [ (idC +₁ extend (τ _) ∘ τ _) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ extend (τ _) ∘ τ _) ∘ i₂ ] ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ ∘[]) ⟩ 
+                (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∎
+              id*∘Dτ : extend idC ∘ extend (now ∘ τ _) ≈ extend (τ _)
+              id*∘Dτ = begin 
+                extend idC ∘ extend (now ∘ τ _) ≈⟨ sym k-assoc ⟩ 
+                extend (extend idC ∘ now ∘ τ _) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩
+                extend (idC ∘ τ _) ≈⟨ extend-≈ identityˡ ⟩ 
+                extend (τ _) ∎
+              tri₂' : (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ
+              tri₂' = begin 
+                (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ∘[]) ⟩ 
+                (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₁) , (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []-cong₂ ⁂∘⁂ ⁂∘⁂ ⟩
+                (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ (idC ∘ idC ⁂ [ out , i₂ ∘ extend idC ] ∘ i₁) , (idC ∘ idC ⁂ [ out , i₂ ∘ extend idC ] ∘ i₂) ] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []-cong₂ (⁂-cong₂ identity² inject₁) (⁂-cong₂ identity² inject₂) ⟩
+                (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ idC ⁂ out , idC ⁂ i₂ ∘ extend idC ] ≈⟨ refl⟩∘⟨ ∘[] ⟩
+                (idC +₁ τ _) ∘ [ distributeˡ⁻¹ ∘ (idC ⁂ out) , distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ ∘[] ⟩
+                [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ sym ([]-cong₂ refl (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩
+                [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂)) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl ((refl⟩∘⟨ dstr-law₂) ⟩∘⟨refl) ⟩
+                [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ _) ∘ i₂) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl (pushˡ +₁∘i₂) ⟩
+                [ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((+₁-cong₂ refl (introʳ (⟨⟩-unique id-comm (id-comm ○ (sym k-identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) refl ⟩
+                [ (idC +₁ τ _ ∘ (idC ⁂ extend idC ∘ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((sym (+₁-cong₂ refl (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩∘⟨refl) refl ⟩
+                [ (idC +₁ τ _ ∘ (idC ⁂ extend idC) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ sym ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² assoc)) +₁∘i₂) ⟩
+                [ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ i₂ ] ≈⟨ sym ∘[] ⟩
+                (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ≈⟨ sym (refl⟩∘⟨ (elimʳ (IsIso.isoˡ isIsoˡ))) ⟩
+                (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ ∎
+              tri₂ : (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ≈ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹
+              tri₂ = iso-epi-from 
+                (record { from = distributeˡ ; to = distributeˡ⁻¹ ; iso = IsIso.iso isIsoˡ }) 
+                ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ])) 
+                ((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) 
+                (assoc ○ refl⟩∘⟨ assoc ○ tri₂' ○ sym-assoc ○ sym-assoc ○ assoc ⟩∘⟨refl)
+
           strength-assoc' : ∀ {X Y Z} → extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ ((X × Y), Z) ≈ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩
           strength-assoc' {X} {Y} {Z} = begin 
             extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y × Z)) (record { f = extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ; commutes = begin 
@@ -487,11 +512,10 @@ Next we will show that the delay monad is strong, by giving a natural transforma
                 (distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ sym (introʳ (IsIso.isoʳ isIsoˡ)) ⟩
                 distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ sym (refl⟩∘⟨ ⁂∘⟨⟩) ⟩
                 distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎)
-{- ⁂ ⊤ ○ 
-Diagram for identityˡ':
-https://q.uiver.app/#q=WzAsOSxbMCwyLCIxIFxcdGltZXMgREIiXSxbMiwyLCIxIFxcdGltZXMgKEIgKyBEQikiXSxbNiwyLCIxIFxcdGltZXMgQiArIDEgXFx0aW1lcyBEQiJdLFswLDQsIkQoMSBcXHRpbWVzIEIpIl0sWzYsNCwiKDEgXFx0aW1lcyBCKSArIEQoMSBcXHRpbWVzIEIpIl0sWzAsNiwiREIiXSxbNiw2LCJCICsgREIiXSxbMCwwLCIxIFxcdGltZXMgREIiXSxbNiwwLCJCICsgMSBcXHRpbWVzIERCIl0sWzAsMSwiaWQgXFx0aW1lcyBvdXQiXSxbMSwyLCJkaXN0cmliXnstMX0iXSxbMCwzLCJcXHRhdSIsMl0sWzUsNiwib3V0IiwyXSxbMyw0LCJvdXQiLDJdLFsyLDQsImlkICsgXFx0YXUiXSxbMyw1LCJEIFxccGlfMiJdLFs0LDYsIlxccGlfMiArIEQgXFxwaV8yIl0sWzcsOCwiKFxccGlfMiArIGlkKSBcXGNpcmMgZGlzdHJpYl57LTF9IFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpIl0sWzcsMCwiaWQiXSxbOCwyLCJcXGxhbmdsZSAhICwgaWQgXFxyYW5nbGUgKyBpZCJdXQ==
--}
--- ⊤
+-- {- ⁂ ⊤ ○ 
+-- Diagram for identityˡ':
+-- https://q.uiver.app/#q=WzAsOSxbMCwyLCIxIFxcdGltZXMgREIiXSxbMiwyLCIxIFxcdGltZXMgKEIgKyBEQikiXSxbNiwyLCIxIFxcdGltZXMgQiArIDEgXFx0aW1lcyBEQiJdLFswLDQsIkQoMSBcXHRpbWVzIEIpIl0sWzYsNCwiKDEgXFx0aW1lcyBCKSArIEQoMSBcXHRpbWVzIEIpIl0sWzAsNiwiREIiXSxbNiw2LCJCICsgREIiXSxbMCwwLCIxIFxcdGltZXMgREIiXSxbNiwwLCJCICsgMSBcXHRpbWVzIERCIl0sWzAsMSwiaWQgXFx0aW1lcyBvdXQiXSxbMSwyLCJkaXN0cmliXnstMX0iXSxbMCwzLCJcXHRhdSIsMl0sWzUsNiwib3V0IiwyXSxbMyw0LCJvdXQiLDJdLFsyLDQsImlkICsgXFx0YXUiXSxbMyw1LCJEIFxccGlfMiJdLFs0LDYsIlxccGlfMiArIEQgXFxwaV8yIl0sWzcsOCwiKFxccGlfMiArIGlkKSBcXGNpcmMgZGlzdHJpYl57LTF9IFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpIl0sWzcsMCwiaWQiXSxbOCwyLCJcXGxhbmdsZSAhICwgaWQgXFxyYW5nbGUgKyBpZCJdXQ==
+-- -}
           commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂) 
             → τ P₂ ∘ ((fst fg) ⁂ extend (now ∘ (snd fg))) ≈ extend (now ∘ ((fst fg) ⁂ (snd fg))) ∘ τ P₁
           commute' {(U , V)} {(W , X)} (f , g) = begin 
@@ -521,7 +545,7 @@ https://q.uiver.app/#q=WzAsOSxbMCwyLCIxIFxcdGltZXMgREIiXSxbMiwyLCIxIFxcdGltZXMgK
               open Terminal (coalgebras (W × X))
               alg' : F-Coalgebra ((W × X) +-)
               alg' = record { A = U × D₀ V ; α = ((f ⁂ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }
--- ⁂ ○ ˡ ʳ 
+
       strongMonad : StrongMonad monoidal
       strongMonad = record { M = monad ; strength = strength }
 ```

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
-
-  module _ (D : DelayM) where
-    open DelayM D
-
-    open Functor functor using () renaming (F₁ to D₁)
-    open RMonad kleisli
-
-    module _ {X : Obj} (coeq : Coequalizer (extend (ι {X})) (D₁ π₁)) where
-      -- TODO
+```
+
+
+# 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 renaming (functor to D-Fun; monad to D-Monad; kleisli to D-Kleisli)
+
+    open Functor D-Fun using () renaming (F₁ to D₁)
+    open RMonad D-Kleisli
+
+
+    
+
+    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 = {!   !}
 ```