From 59492a950246a61f989024887fcfcfd55134580f Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Wed, 27 Sep 2023 20:06:46 +0200
Subject: [PATCH] Progress on strength for delay monad

---
 .../Instance/AmbientCategory.lagda.md         |   4 +-
 src/Monad/Instance/Delay.lagda.md             | 107 +++++++++++++++---
 2 files changed, 94 insertions(+), 17 deletions(-)

diff --git a/src/Category/Instance/AmbientCategory.lagda.md b/src/Category/Instance/AmbientCategory.lagda.md
index db4a496..c04bbfc 100644
--- a/src/Category/Instance/AmbientCategory.lagda.md
+++ b/src/Category/Instance/AmbientCategory.lagda.md
@@ -50,7 +50,9 @@ module Category.Instance.AmbientCategory where
     -- open Terminal terminal public
     -- Don't open the terminal object, because we are interested in many different terminal objects stemming from multiple categories
     open BinaryProducts products renaming (η to ⁂-η; g-η to ⁂-g-η; unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′) public
-    open ParametrizedNNO ℕ public
+    open ParametrizedNNO ℕ public renaming (η to pnno-η)
+
+    open CartesianMonoidal cartesian using (⊤×A≅A; A×⊤≅A) public
 
 
     distributive : Distributive C
diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md
index bce4d1b..ed6e188 100644
--- a/src/Monad/Instance/Delay.lagda.md
+++ b/src/Monad/Instance/Delay.lagda.md
@@ -1,5 +1,6 @@
 <!--
 ```agda
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Categories.Category
 open import Categories.Monad
@@ -294,30 +295,41 @@ 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)
+      open RMonad kleisli using (extend) renaming (assoc to k-assoc)
       open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_)
+      open Monad monad using () renaming (η to η'; μ to μ')
+      module η = NaturalTransformation η'
+      module μ = NaturalTransformation μ'
       strength : Strength monoidal monad
       strength = record
         { strengthen = ntHelper (record 
           { η = τ
           ; commute = commute' })
-        ; identityˡ = λ {X} → begin 
-          extend (now ∘ π₂) ∘ τ _ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
-          (out⁻¹ ∘ out) ∘ extend (now ∘ π₂) ∘ τ _ ≈⟨ pullʳ (pullˡ (extendlaw (now ∘ π₂))) ⟩
-          out⁻¹ ∘ ([ out ∘ now ∘ π₂ , i₂ ∘ extend (now ∘ π₂)] ∘ out) ∘ τ _ ≈⟨ refl⟩∘⟨ (pullʳ (τ-law (Terminal.⊤ terminal , X))) ⟩
-          out⁻¹ ∘ [ out ∘ now ∘ π₂ , i₂ ∘ extend (now ∘ π₂)] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ {! refl⟩∘⟨_  !} ⟩
-          {!   !} ≈⟨ {!   !} ⟩
-          {!   !} ≈⟨ {!   !} ⟩
-          {!   !} ≈⟨ {!   !} ⟩
-          {!   !} ≈⟨ {!   !} ⟩
-          -- TODO extend and τ are both final coalgebras, maybe use this?
-          π₂ ∎ 
-        ; η-comm = {!   !}
-        ; μ-η-comm = {!   !}
+        ; identityˡ = identityˡ'
+        ; η-comm = begin 
+          τ _ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂) ⟩ 
+          τ _ ∘ (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 ∎
+        ; μ-η-comm = begin 
+          extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈⟨ pullˡ (sym k-assoc) ⟩ 
+          extend (extend idC ∘ now ∘ τ _) ∘ τ _ ≈⟨ {!   !} ⟩ 
+          {!   !} ≈⟨ {!   !} ⟩ 
+          τ _ ∘ (idC ⁂ extend idC) ∎
         ; strength-assoc = {!   !}
         }
         where
           open import Agda.Builtin.Sigma
+          out-law : ∀ {X Y} (f : X ⇒ Y) → out {Y} ∘ extend (now ∘ f) ≈ (f +₁ extend (now ∘ f)) ∘ out {X}
+          out-law {X} {Y} f = begin 
+            out ∘ extend (now ∘ f) ≈⟨ extendlaw (now ∘ f) ⟩ 
+            [ out ∘ now ∘ f , i₂ ∘ extend (now ∘ f) ] ∘ out ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩
+            (f +₁ extend (now ∘ f)) ∘ out ∎
+          dstr-law : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₁) ≈ i₁
+          dstr-law = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ))
+
           module _ (P : Category.Obj (CProduct C C)) where
             X = fst P
             Y = snd P
@@ -329,9 +341,73 @@ Next we will show that the delay monad is strong, by giving a natural transforma
             τ-law : out ∘ τ ≈ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
             τ-law = commutes (! {A = record { A = X × D₀ Y ; α = distributeˡ⁻¹ ∘ (idC ⁂ out) }})
 
+            τ-helper : τ ∘ (idC ⁂ out⁻¹) ≈ out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹
+            τ-helper = begin 
+              τ ∘ (idC ⁂ out⁻¹) ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩ 
+              (out⁻¹ ∘ out) ∘ τ ∘ (idC ⁂ out⁻¹) ≈⟨ pullʳ (pullˡ τ-law) ⟩
+              out⁻¹ ∘ ((idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ out⁻¹) ≈⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ assoc) ⟩
+              out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ (idC ⁂ out⁻¹) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimʳ (⁂∘⁂ ○ (⁂-cong₂ identity² (_≅_.isoʳ out-≅)) ○ ((⟨⟩-cong₂ identityˡ identityˡ) ○ ⁂-η)))) ⟩
+              out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∎
+
+            τ-helper₂ : out ∘ extend (now ∘ π₂) ∘ τ ≈ out ∘ π₂
+            τ-helper₂ = begin 
+              out ∘ extend (now ∘ π₂) ∘ τ ≈⟨ pullˡ (extendlaw (now ∘ π₂)) ⟩ 
+              ([ out ∘ now ∘ π₂ , i₂ ∘ extend (now ∘ π₂)] ∘ out) ∘ τ ≈⟨ (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl) ⟩∘⟨refl ⟩
+              ((π₂ +₁ extend (now ∘ π₂)) ∘ out) ∘ τ ≈⟨ pullʳ τ-law ⟩
+              (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩
+              (π₂ ∘ idC +₁ extend (now ∘ π₂) ∘ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ identityʳ refl) ⟩∘⟨refl ⟩
+              (π₂ +₁ extend (now ∘ π₂) ∘ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ {!   !} ⟩
+              {!   !} ≈⟨ {!   !} ⟩
+              {!   !} ≈⟨ {!   !} ⟩
+              out ∘ π₂ ∎ 
+
             τ-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 }))
 
+          identityˡ' : ∀ {X : Obj} → extend (now ∘ π₂) ∘ τ (Terminal.⊤ terminal , X) ≈ π₂
+          identityˡ' {X} = begin
+            extend (now ∘ π₂) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras X) {A = record { A = Terminal.⊤ terminal × D₀ X ; α = (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }} (record { f = extend (now ∘ π₂) ∘ τ _ ; commutes = begin 
+              out ∘ extend (now ∘ π₂) ∘ τ _ ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (sym identityʳ)) ⟩ 
+              out ∘ extend (now ∘ π₂) ∘ τ _ ∘ idC ≈⟨ pullˡ diag₃ ⟩ 
+              ((π₂ +₁ extend (now ∘ π₂)) ∘ out) ∘ τ _ ∘ idC ≈⟨ pullʳ (pullˡ (diag₂ (Terminal.⊤ terminal , X))) ⟩ 
+              (π₂ +₁ extend (now ∘ π₂)) ∘ ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ idC ≈⟨ refl⟩∘⟨ (pullʳ (assoc ○ sym diag₁)) ⟩ 
+              (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ○ CC.+-unique ((identity² ⟩∘⟨refl) ○ id-comm-sym) ((identity² ⟩∘⟨refl) ○ id-comm-sym)) ) ⟩ 
+              (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩ 
+              (π₂ ∘ idC +₁ extend (now ∘ π₂) ∘ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ id-comm refl) ⟩∘⟨refl ⟩ 
+              (idC ∘ π₂ +₁ extend (now ∘ π₂) ∘ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullˡ +₁∘+₁ ⟩ 
+              (idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimˡ identity²)) ⟩ 
+              (idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ refl⟩∘⟨ ((+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl) ⟩ 
+              (idC +₁ extend (now ∘ π₂)) ∘ (idC ∘ π₂ +₁ τ _ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullʳ (pullˡ +₁∘+₁) ⟩ 
+              ((idC +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _)) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ (homomorphism (X +-)) ⟩∘⟨refl ⟩ 
+              (idC +₁ extend (now ∘ π₂) ∘ τ _) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩
+            u (Terminal.! (coalgebras X)) ≈⟨ Terminal.!-unique (coalgebras X) {A = record { A = Terminal.⊤ terminal × D₀ X ; α = (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }} (record { f = π₂ ; commutes = begin 
+              out ∘ π₂ ≈˘⟨ π₂∘⁂ ⟩ 
+              π₂ ∘ (idC ⁂ out) ≈˘⟨ pullˡ distribute₂ ⟩ -- TODO this might be wrong if distribute₂ is unprovable
+              (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ (+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl ⟩ 
+              (idC ∘ π₂ +₁ π₂ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullˡ +₁∘+₁ ⟩ 
+              (idC +₁ π₂) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩
+            π₂ ∎ 
+            where
+              diag₁ : (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈ distributeˡ⁻¹ {Terminal.⊤ terminal} {X} {D₀ X} ∘ (idC ⁂ out) ∘ idC
+              diag₁ = begin 
+                (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩ 
+                (⟨ Terminal.! terminal , idC ⟩ ∘ π₂ +₁ idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ⟩∘⟨ (refl⟩∘⟨ sym identityʳ) ⟩ 
+                (idC +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC ≈⟨ elimˡ (CC.+-unique id-comm-sym id-comm-sym) ⟩ 
+                distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC ∎
+              diag₂ = τ-law
+              diag₃ : out {X} ∘ extend (now ∘ π₂ {A = Terminal.⊤ terminal} {B = X}) ≈ (π₂ +₁ extend (now ∘ π₂)) ∘ out
+              diag₃ = out-law π₂
+              distribute₂ : ∀ {A B C} → (π₂ +₁ π₂) ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₂
+              distribute₂ = sym (begin 
+                π₂ ≈⟨ introʳ (IsIso.isoʳ isIsoˡ) ⟩ 
+                π₂ ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ pullˡ ∘[] ⟩
+                [ π₂ ∘ ((idC ⁂ i₁)) , π₂ ∘ (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ π₂∘⁂ π₂∘⁂) ⟩∘⟨refl ⟩
+                (π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∎)
+{- ⁂ ⊤
+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 
@@ -371,8 +447,7 @@ Next we will show that the delay monad is strong, by giving a natural transforma
                 (distributeˡ⁻¹ ∘ [ ((f ⁂ (g +₁ h)) ∘ (idC ⁂ i₁)) , ((f ⁂ (g +₁ h)) ∘ (idC ⁂ i₂)) ]) ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ (pullʳ ∘[])) ⟩
                 (distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h))) ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ sym (introʳ (IsIso.isoʳ isIsoˡ)) ⟩
                 distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h)) ∎
--- ⁂ ○ ˡ
+-- ⁂ ○ ˡ ʳ 
       strongMonad : StrongMonad monoidal
       strongMonad = record { M = monad ; strength = strength }
 ```
-