minor

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