From bb2e7c5061fe57af599bd7ab5cca302d243b9520 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Wed, 22 Nov 2023 09:44:20 +0100
Subject: [PATCH] Work on commutativity

---
 src/Algebra/Elgot.lagda.md                |  2 ++
 src/Monad/Instance/K/Commutative.lagda.md | 40 +++++++++++------------
 2 files changed, 22 insertions(+), 20 deletions(-)

diff --git a/src/Algebra/Elgot.lagda.md b/src/Algebra/Elgot.lagda.md
index 7eeb2da..a7c9ed5 100644
--- a/src/Algebra/Elgot.lagda.md
+++ b/src/Algebra/Elgot.lagda.md
@@ -112,6 +112,8 @@ Here we give a different Characterization and show that it is equal.
       ⟩
       ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂  ∎
 
+    -- TODO Proposition 41
+
     -- every elgot-algebra comes with a divergence constant
     !ₑ : ⊥ ⇒ A
     !ₑ = i₂ #
diff --git a/src/Monad/Instance/K/Commutative.lagda.md b/src/Monad/Instance/K/Commutative.lagda.md
index 3534f58..687a8b1 100644
--- a/src/Monad/Instance/K/Commutative.lagda.md
+++ b/src/Monad/Instance/K/Commutative.lagda.md
@@ -164,6 +164,12 @@ KCommutative = record { commutes = commutes' }
           where
             ψ : ∀ {X Y} → K.₀ X × K.₀ Y ⇒ K.₀ (X × Y)
             ψ = extend (τ _) ∘ σ _
+            ψ-left-iter : ∀ {X Y U} (h : X ⇒ K.₀ Y + X) → ψ {Y} {U} ∘ (h # ⁂ idC) ≈ ((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #
+            ψ-left-iter {X} {Y} {U} h = begin 
+              ψ ∘ (h # ⁂ idC) ≈⟨ pullʳ (σ-comm h) ⟩ 
+              extend (τ _) ∘ ((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))# ≈⟨ extend-preserve (τ (Y , U)) (((σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))) ⟩ 
+              ((extend (τ _) +₁ idC) ∘ (σ _ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC))# ≈⟨ #-resp-≈ (algebras (Y × U)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩ 
+              (((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (h ⁂ idC)) #) ∎
             comm₅ : (ψ ∘ (idC ⁂ (h #))) ∘ (η _ ⁂ idC) ≈ τ _ ∘ (idC ⁂ h #)
             comm₅ = begin 
               (ψ ∘ (idC ⁂ (h #))) ∘ (η _ ⁂ idC) ≈⟨ pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm) ⟩ 
@@ -204,25 +210,19 @@ KCommutative = record { commutes = commutes' }
                   (idC +₁ (idC ⁂ h #)) ∘ ((ψ ∘ (idC ⁂ h #)) +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) ∎
             comm₈ : ∀ {U} (g : U ⇒ K.₀ X + U) → ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∘ (g # ⁂ idC) ≈ ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))#
             comm₈ {U} g = begin
-              ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ {!!} ⟩ -- Uniformity
-              ((((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ {!   !} ⟩
-              ( [ (idC +₁ i₁) ∘ (ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ [ i₁ , distributeˡ⁻¹ ∘ (idC ⁂ h) ]) # ∘ i₂ ≈⟨ {!!} ⟩
-              ([ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ [ i₁ , distributeˡ⁻¹ ∘ (idC ⁂ h) ]) # ∘ i₂ ≈⟨ {!!} ⟩
-              [ [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ i₁ , [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ] # ∘ i₂ ≈⟨ {!!} ⟩
-              [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ] # ∘ i₂ ≈⟨ {!!} ⟩
-              ([ (ψ +₁ i₁) ∘ distributeʳ⁻¹ , [ (ψ +₁ i₁) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC) , i₂ ∘ i₂ ] ∘ distributeˡ⁻¹ ] ∘ (g ⁂ idC +₁ idC ⁂ h)) # ∘ i₂ ≈⟨ {!!} ⟩
-              {!!} ≈⟨ {!!} ⟩
-              {!!} ≈⟨ {!!} ⟩
-              {!!} ≈⟨ {!!} ⟩
-              {!!} ≈⟨ {!!} ⟩
-              {!!} ≈⟨ {!!} ⟩
-              {!!} ≈⟨ {!!} ⟩
-              ([((ψ +₁ i₁) ∘ distributeʳ⁻¹) , (i₂ ∘ i₂ ∘ distributeʳ⁻¹) ] ∘ distributeˡ⁻¹ ∘ {!!}) # ∘ i₂ ∘ i₂ ≈⟨ {!!} ⟩
-              {!!} ≈˘⟨ {!!} ⟩
-              {!!} ≈˘⟨ {!!} ⟩
-              {!!} ≈˘⟨ {!!} ⟩
-              {!!} ≈˘⟨ {!!} ⟩
-              ([ (idC +₁ i₁) ∘ (ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) , i₂ ∘ i₂ ] ∘ [ i₁ , distributeʳ⁻¹ ∘ (g ⁂ idC) ]) # ∘ i₂ ≈˘⟨ {!   !} ⟩
+              ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∘ (g # ⁂ idC) ≈⟨ sym (#-Uniformity (algebras (X × Y)) (sym by-uni)) ⟩ 
+              ((ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ (ψ-left-iter g) refl) ⟩∘⟨refl) ⟩
+              (((((ψ +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC)) # +₁ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ {!   !} ⟩
+              {!   !} ≈⟨ {!   !} ⟩
+              {!   !} ≈⟨ {!   !} ⟩
+              {!   !} ≈⟨ {!   !} ⟩
               ((((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# +₁ idC) ∘ distributeʳ⁻¹ ∘ (g ⁂ idC))# ∎
-
+              where
+                by-uni : ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ((g #) ⁂ idC) ≈ (idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)
+                by-uni = begin 
+                  ((ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) ∘ ((g #) ⁂ idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ id-comm-sym id-comm ○ sym ⁂∘⁂)) ⟩ 
+                  (ψ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((g #) ⁂ idC) ∘ (idC ⁂ h) ≈⟨ {!   !} ⟩ 
+                  (ψ +₁ idC) ∘ ((((g #) ⁂ idC) +₁ ((g #) ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (sym identityˡ) id-comm-sym ○ sym +₁∘+₁)) ⟩ 
+                  (((idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h) ≈⟨ assoc² ⟩ 
+                  (idC +₁ (g #) ⁂ idC) ∘ (ψ ∘ ((g #) ⁂ idC) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ∎
 ```