diff --git a/src/Algebra/Elgot.lagda.md b/src/Algebra/Elgot.lagda.md
index 33abec5..c8c086f 100644
--- a/src/Algebra/Elgot.lagda.md
+++ b/src/Algebra/Elgot.lagda.md
@@ -139,7 +139,6 @@ Here we give a different Characterization and show that it is equal.
           [ (idC +₁ (i₁ +₁ idC)) ∘ i₁ ∘ h , (idC +₁ (i₁ +₁ idC)) ∘ [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ]                        ≈˘⟨ ∘[] ⟩
           (idC +₁ (i₁ +₁ idC)) ∘ [ i₁ ∘ h , [ (h +₁ i₁) , i₂ ∘ i₂ ] ∘ f ]                                               ∎
 
-    -- 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 #                                                                                                             ≈⟨ introʳ inject₂ ⟩ 
@@ -153,7 +152,8 @@ Here we give a different Characterization and show that it is equal.
       [ i₁ , [ [ (idC +₁ i₁) ∘ i₁ , (i₂ ∘ i₂) ∘ i₁ ] ∘ g , [ (idC +₁ i₁) ∘ i₂ , (i₂ ∘ i₂) ∘ idC ] ∘ f ] ] # ∘ i₂ ∘ i₂ ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (([]-cong₂ (+₁∘i₁ ○ identityʳ) assoc) ⟩∘⟨refl) (([]-cong₂ +₁∘i₂ identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩ 
       [ i₁ , [ [ i₁ , i₂ ∘ i₂ ∘ i₁ ] ∘ g , [ i₂ ∘ i₁ , i₂ ∘ i₂ ] ∘ f ] ] # ∘ i₂ ∘ i₂                                  ≈˘⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (pullˡ ([]∘+₁ ○ []-cong₂ identityʳ refl)) (∘[] ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩
       [ i₁ , [ [ i₁ , i₂ ] ∘ (idC +₁ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ , i₂ ]) ∘ f ] ] # ∘ i₂ ∘ i₂                            ≈⟨ ((#-resp-≈ ([]-cong₂ refl ([]-cong₂ (elimˡ +-η) ((elimʳ +-η) ⟩∘⟨refl)))) ⟩∘⟨refl) ⟩ 
-      [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂ {A = X} {B = X}                                          ≈⟨ {!   !} ⟩
+      [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] # ∘ i₂ ∘ i₂                                                          ≈˘⟨ pullˡ (sym (#-Uniformity by-uni₂)) ⟩
+      [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ i₂ ∘ i₂                                ≈⟨ (refl⟩∘⟨ (pullˡ inject₂ ○ (+₁∘i₂ ○ identityʳ))) ⟩
       [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂ {A = A + X} {B = X}                                           ≈˘⟨ ((#-resp-≈ ([]-cong₂ (∘[] ○ []-cong₂ (+₁∘i₁ ○ identityʳ) (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl))) refl)) ⟩∘⟨refl) ⟩ 
       [ (idC +₁ i₁) ∘ [ i₁ , (idC +₁ i₂) ∘ g ] , i₂ ∘ h ] # ∘ i₂                                                      ≈⟨ (sym #-Folding) ⟩∘⟨refl ⟩ 
       ([ i₁ , (idC +₁ i₂) ∘ g ] # +₁ h)# ∘ i₂                                                                         ≈⟨ ((#-resp-≈ (+₁-cong₂ by-fix refl)) ⟩∘⟨refl) ⟩ 
@@ -167,13 +167,24 @@ Here we give a different Characterization and show that it is equal.
       where
         g = (idC +₁ [ idC , idC ]) ∘ f
         h = [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ f
+        by-uni₂ : (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ] ≈ [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ]
+        by-uni₂ = begin 
+          (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ [ i₁ , [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ]                                       ≈⟨ ∘[] ⟩ 
+          [ (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ i₁ , (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ [ (idC +₁ i₂ ∘ i₁) ∘ g , i₂ ∘ f ] ]    ≈⟨ []-cong₂ (+₁∘i₁ ○ identityʳ) ∘[] ⟩ 
+          [ i₁ , [ (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ (idC +₁ i₂ ∘ i₁) ∘ g , (idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ i₂ ∘ f ] ]    ≈⟨ []-cong₂ refl ([]-cong₂ (pullˡ +₁∘+₁) (pullˡ +₁∘i₂)) ⟩ 
+          [ i₁ , [ (idC ∘ idC +₁ [ i₁ ∘ i₁ , i₂ +₁ idC ] ∘ i₂ ∘ i₁) ∘ g , (i₂ ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ]) ∘ f ] ]              ≈⟨ []-cong₂ refl ([]-cong₂ ((+₁-cong₂ identity² (pullˡ inject₂ ○ +₁∘i₁)) ⟩∘⟨refl) (∘[] ⟩∘⟨refl)) ⟩ 
+          [ i₁ , [ (idC +₁ i₁ ∘ i₂) ∘ g , [ i₂ ∘ i₁ ∘ i₁ , i₂ ∘ (i₂ +₁ idC) ] ∘ f ] ]                                         ≈˘⟨ []-cong₂ refl ([]-cong₂ refl (pullˡ ∘[])) ⟩ 
+          [ i₁ , [ (idC +₁ i₁ ∘ i₂) ∘ g , i₂ ∘ h ] ]                                                                          ≈˘⟨ []-cong₂ inject₁ ([]-cong₂ inject₂ identityʳ) ⟩ 
+          [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] ∘ i₁ , [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] ∘ i₂ , (i₂ ∘ h) ∘ idC ] ]                    ≈˘⟨ []-cong₂ (pullˡ inject₁) []∘+₁ ⟩ 
+          [ [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ i₁ ∘ i₁ , [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ (i₂ +₁ idC) ] ≈˘⟨ ∘[] ⟩ 
+          [ [ i₁ , (idC +₁ i₁ ∘ i₂) ∘ g ] , i₂ ∘ h ] ∘ [ i₁ ∘ i₁ , i₂ +₁ idC ]                                                ∎
         by-uni₁ : (idC +₁ [ idC , idC ]) ∘ [ (idC +₁ i₁) ∘ g , f ] ≈ g ∘ [ idC , idC ]
         by-uni₁ = begin 
-          (idC +₁ [ idC , idC ]) ∘ [ (idC +₁ i₁) ∘ g , f ] ≈⟨ ∘[] ⟩ 
+          (idC +₁ [ idC , idC ]) ∘ [ (idC +₁ i₁) ∘ g , f ]                          ≈⟨ ∘[] ⟩ 
           [ (idC +₁ [ idC , idC ]) ∘ (idC +₁ i₁) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ] ≈⟨ []-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² inject₁)) refl ⟩ 
-          [ (idC +₁ idC) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ] ≈⟨ []-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) refl ⟩ 
-          [ g , g ] ≈⟨ sym (∘[] ○ []-cong₂ identityʳ identityʳ) ⟩ 
-          g ∘ [ idC , idC ] ∎
+          [ (idC +₁ idC) ∘ g , (idC +₁ [ idC , idC ]) ∘ f ]                         ≈⟨ []-cong₂ (elimˡ ([]-unique id-comm-sym id-comm-sym)) refl ⟩ 
+          [ g , g ]                                                                 ≈⟨ sym (∘[] ○ []-cong₂ identityʳ identityʳ) ⟩ 
+          g ∘ [ idC , idC ]                                                         ∎
         by-fix : [ i₁ , (idC +₁ i₂) ∘ g ] # ≈ [ idC , g # ]
         by-fix = sym (begin 
           [ idC , g # ]                                                   ≈⟨ []-cong₂ refl #-Fixpoint ⟩