From 2317c6b30d1a231beff20021850a1ccf076b0cb5 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Wed, 22 Nov 2023 09:58:20 +0100
Subject: [PATCH] minor

---
 src/Algebra/Elgot.lagda.md | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/Algebra/Elgot.lagda.md b/src/Algebra/Elgot.lagda.md
index a7c9ed5..c305bfc 100644
--- a/src/Algebra/Elgot.lagda.md
+++ b/src/Algebra/Elgot.lagda.md
@@ -113,6 +113,18 @@ Here we give a different Characterization and show that it is equal.
       ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂  ∎
 
     -- TODO Proposition 41
+    #-Diamond : ∀ {X} (f : X ⇒ A + (X + X)) → ((idC +₁ [ idC , idC ]) ∘ f)# ≈ ([ i₁ , ((idC +₁ [ idC , idC ]) ∘ f) # +₁ idC ] ∘ f) #
+    #-Diamond {X} f = begin 
+      g # ≈⟨ {!   !} ⟩ 
+      {!   !} ≈⟨ {!   !} ⟩ 
+      {!   !} ≈⟨ {!   !} ⟩ 
+      [ (idC +₁ i₁) ∘ [ i₁ , (idC +₁ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ ≈⟨ (sym #-Folding) ⟩∘⟨refl ⟩ 
+      ([ i₁ , (idC +₁ i₂) ∘ g ] # +₁ h)# ∘ i₂ ≈⟨ {!   !} ⟩ 
+      {!   !} ≈⟨ {!   !} ⟩ 
+      ([ i₁ , g # +₁ idC ] ∘ f) # ∎
+      where
+        g = (idC +₁ [ idC , idC ]) ∘ f
+        h = [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ f
 
     -- every elgot-algebra comes with a divergence constant
     !ₑ : ⊥ ⇒ A