From 0be1871679e115b634cf651aafd0e00e7ed0ca09 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Tue, 25 Jul 2023 17:23:36 +0200
Subject: [PATCH] Indentation

---
 ElgotAlgebra.agda  | 127 ++++++++++++++++++++--------------------
 ElgotAlgebras.agda | 141 +++++++++++++++++++++++----------------------
 2 files changed, 137 insertions(+), 131 deletions(-)

diff --git a/ElgotAlgebra.agda b/ElgotAlgebra.agda
index cad0edd..d7203d6 100644
--- a/ElgotAlgebra.agda
+++ b/ElgotAlgebra.agda
@@ -37,7 +37,9 @@ module _ (C𝒞 : CocartesianCategory o ℓ e) where
                     → f # ≈ g # ∘ h
                 #-Compositionality : ∀ {X Y} {f : X ⇒ A + F₀ X} {h : Y ⇒ X + F₀ Y}
                     → (((f #) +₁ idC) ∘ h)# ≈ ([ (idC +₁ (F₁ i₁)) ∘ f , i₂ ∘ (F₁ i₂) ] ∘ [ i₁ , h ])# ∘ i₂
-                #-resp-≈ : ∀ {X} {f g : X ⇒ A + F₀ X} → f ≈ g → (f #) ≈ (g #)
+                #-resp-≈ : ∀ {X} {f g : X ⇒ A + F₀ X} 
+                    → f ≈ g 
+                    → (f #) ≈ (g #)
 
     --*
     -- (unguarded) Elgot-Algebra
@@ -71,37 +73,38 @@ module _ (C𝒞 : CocartesianCategory o ℓ e) where
             #-Compositionality {X} {Y} {f} {h} = begin 
                 (((f #) +₁ idC) ∘ h)# ≈⟨ #-Uniformity {f = ((f #) +₁ idC) ∘ h} {g = (f #) +₁ h} {h = h} (
                     begin 
-                    ((idC +₁ h) ∘ ((f #) +₁ idC) ∘ h) ≈⟨ sym-assoc ⟩
-                    (((idC +₁ h) ∘ ((f #) +₁ idC)) ∘ h) ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩ 
+                    ((idC +₁ h) ∘ ((f #) +₁ idC) ∘ h)    ≈⟨ sym-assoc ⟩
+                    (((idC +₁ h) ∘ ((f #) +₁ idC)) ∘ h)  ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩ 
                     ((((idC ∘ (f #)) +₁ (h ∘ idC))) ∘ h) ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩ 
-                    ((((f #) +₁ h)) ∘ h) ∎)
+                    ((((f #) +₁ h)) ∘ h)                 ∎)
                 ⟩ 
                 ((f # +₁ h)# ∘ h) ≈⟨ sym inject₂ ⟩
-                (([ idC ∘ (f #) , (f # +₁ h)# ∘ h ] ∘ i₂)) ≈⟨ ∘-resp-≈ˡ (sym $ []∘+₁) ⟩
-                (([ idC , ((f # +₁ h)#) ] ∘ (f # +₁ h)) ∘ i₂) ≈⟨ (sym $ ∘-resp-≈ˡ (#-Fixpoint {f = (f # +₁ h) })) ⟩
-                (f # +₁ h)# ∘ i₂ ≈⟨ ∘-resp-≈ˡ #-Folding ⟩
-                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂) ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩
+                (([ idC ∘ (f #) , (f # +₁ h)# ∘ h ] ∘ i₂))                                     ≈⟨ ∘-resp-≈ˡ (sym $ []∘+₁) ⟩
+                (([ idC , ((f # +₁ h)#) ] ∘ (f # +₁ h)) ∘ i₂)                                  ≈⟨ (sym $ ∘-resp-≈ˡ (#-Fixpoint {f = (f # +₁ h) })) ⟩
+                (f # +₁ h)# ∘ i₂                                                               ≈⟨ ∘-resp-≈ˡ #-Folding ⟩
+                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂)                                          ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩
                 ([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₂ ≈⟨ assoc ⟩
                 [ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂) ≈⟨ ∘-resp-≈ʳ inject₂ ⟩ 
-                [ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ (i₂ ∘ h) ≈⟨ sym-assoc ⟩ 
-                (([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂) ∘ h) ≈⟨ ∘-resp-≈ˡ inject₂ ⟩ 
-                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h) ≈⟨ ∘-resp-≈ʳ $ sym (inject₂ {f = i₁} {g = h}) ⟩ 
-                [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ ([ i₁ , h ] ∘ i₂) ≈⟨ sym-assoc ⟩ 
-                (([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ]) ∘ i₂) ≈⟨ sym (∘-resp-≈ˡ (#-Uniformity {f = [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]} {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]} {h = [ i₁ , h ]} (
+                [ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ (i₂ ∘ h)                            ≈⟨ sym-assoc ⟩ 
+                (([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂) ∘ h)                          ≈⟨ ∘-resp-≈ˡ inject₂ ⟩ 
+                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h)                                           ≈⟨ ∘-resp-≈ʳ $ sym (inject₂ {f = i₁} {g = h}) ⟩ 
+                [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ ([ i₁ , h ] ∘ i₂)                             ≈⟨ sym-assoc ⟩ 
+                (([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ]) ∘ i₂)                           ≈⟨ sym (∘-resp-≈ˡ (#-Uniformity {f = [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]} {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]} {h = [ i₁ , h ]} (
                     begin 
-                        (idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈⟨ ∘-resp-≈ʳ ∘[] ⟩ 
-                        (idC +₁ [ i₁ , h ]) ∘ [ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ] ≈⟨ ∘-resp-≈ʳ ([]-congʳ inject₁) ⟩ 
-                        ((idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ]) ≈⟨ ∘[] ⟩ 
-                        [ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f) , (idC +₁ [ i₁ , h ]) ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h) ] ≈⟨ []-cong₂ sym-assoc sym-assoc ⟩ 
-                        [ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f , ((idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ]) ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ ∘[]) ⟩ 
+                        (idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]                                                                 ≈⟨ ∘-resp-≈ʳ ∘[] ⟩ 
+                        (idC +₁ [ i₁ , h ]) ∘ [ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ]                                 ≈⟨ ∘-resp-≈ʳ ([]-congʳ inject₁) ⟩ 
+                        ((idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ])                                                  ≈⟨ ∘[] ⟩ 
+                        [ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f) , (idC +₁ [ i₁ , h ]) ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h) ]                          ≈⟨ []-cong₂ sym-assoc sym-assoc ⟩ 
+                        [ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f , ((idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ]) ∘ h ]                          ≈⟨ []-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ ∘[]) ⟩ 
                         [ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f , ([ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f) , (idC +₁ [ i₁ , h ]) ∘ (i₂ ∘ i₂) ]) ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² (inject₁))) (∘-resp-≈ˡ ([]-cong₂ sym-assoc sym-assoc)) ⟩ 
-                        [ (idC +₁ i₁) ∘ f , ([ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f , ((idC +₁ [ i₁ , h ]) ∘ i₂) ∘ i₂ ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ inject₂))) ⟩ 
-                        [ (idC +₁ i₁) ∘ f , ([ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f , (i₂ ∘ [ i₁ , h ]) ∘ i₂ ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁)) assoc)) ⟩ 
-                        [ (idC +₁ i₁) ∘ f , ([ (idC +₁ i₁) ∘ f , i₂ ∘ ([ i₁ , h ] ∘ i₂) ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-congˡ (∘-resp-≈ʳ inject₂))) ⟩ 
-                        [ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ []-congʳ (sym (inject₁)) ⟩ 
-                        [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ sym ∘[] ⟩ 
-                        [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ] ∎))) ⟩
-                ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂  ∎
+                        [ (idC +₁ i₁) ∘ f , ([ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f , ((idC +₁ [ i₁ , h ]) ∘ i₂) ∘ i₂ ]) ∘ h ]                        ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ inject₂))) ⟩ 
+                        [ (idC +₁ i₁) ∘ f , ([ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f , (i₂ ∘ [ i₁ , h ]) ∘ i₂ ]) ∘ h ]                                  ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁)) assoc)) ⟩ 
+                        [ (idC +₁ i₁) ∘ f , ([ (idC +₁ i₁) ∘ f , i₂ ∘ ([ i₁ , h ] ∘ i₂) ]) ∘ h ]                                                         ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-congˡ (∘-resp-≈ʳ inject₂))) ⟩ 
+                        [ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ]                                                                           ≈⟨ []-congʳ (sym (inject₁)) ⟩ 
+                        [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ]                                                         ≈⟨ sym ∘[] ⟩ 
+                        [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ]                                                                                        ∎))
+                    )⟩
+                ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂                             ∎
 
             -- every elgot-algebra comes with a divergence constant
             !ₑ : ⊥ ⇒ A
@@ -130,7 +133,7 @@ module _ (C𝒞 : CocartesianCategory o ℓ e) where
         { _# = _#
         ; #-Fixpoint = λ {X} {f} → begin 
                 f # ≈⟨ #-Fixpoint ⟩ 
-                [ idC , f # ] ∘ f ≈⟨ sym $ ∘-resp-≈ˡ ([]-congˡ identityˡ) ⟩ 
+                [ idC , f # ] ∘ f       ≈⟨ sym $ ∘-resp-≈ˡ ([]-congˡ identityˡ) ⟩ 
                 [ idC , idC ∘ f # ] ∘ f ∎
         ; #-Uniformity = #-Uniformity
         ; #-Compositionality = #-Compositionality
@@ -148,13 +151,13 @@ module _ (C𝒞 : CocartesianCategory o ℓ e) where
         ; #-Fixpoint = λ {X} {f} → begin 
                 f # ≈⟨ #-Fixpoint ⟩ 
                 [ idC , idC ∘ f # ] ∘ f ≈⟨ ∘-resp-≈ˡ ([]-congˡ identityˡ) ⟩ 
-                [ idC , f # ] ∘ f ∎
+                [ idC , f # ] ∘ f       ∎
         ; #-Uniformity = #-Uniformity
         ; #-Folding = λ {X} {Y} {f} {h} → begin 
-            ((f #) +₁ h) # ≈⟨ sym +-g-η ⟩ 
-            [ (f # +₁ h)# ∘ i₁ , (f # +₁ h)# ∘ i₂ ] ≈⟨ []-cong₂ left right ⟩ 
+            ((f #) +₁ h) #                                                                ≈⟨ sym +-g-η ⟩ 
+            [ (f # +₁ h)# ∘ i₁ , (f # +₁ h)# ∘ i₂ ]                                       ≈⟨ []-cong₂ left right ⟩ 
             [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂ ] ≈⟨ +-g-η ⟩ 
-            ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] #) ∎
+            ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] #)                                              ∎
         ; #-resp-≈ = #-resp-≈
         }
         where 
@@ -164,51 +167,53 @@ module _ (C𝒞 : CocartesianCategory o ℓ e) where
             left : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} 
                 → (f # +₁ h)# ∘ i₁ ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁
             left {X} {Y} {f} {h} = begin  
-                (f # +₁ h)# ∘ i₁ ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩ 
+                (f # +₁ h)# ∘ i₁                                         ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩ 
                 (([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₁) ≈⟨ assoc ⟩ 
                 ([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ (((f #) +₁ h) ∘ i₁)) ≈⟨ ∘-resp-≈ ([]-congˡ identityˡ) +₁∘i₁ ⟩
-                ([ idC , ((f #) +₁ h) # ] ∘ (i₁ ∘ (f #))) ≈⟨ sym-assoc ⟩
-                (([ idC , ((f #) +₁ h) # ] ∘ i₁) ∘ (f #)) ≈⟨ ∘-resp-≈ˡ inject₁ ⟩
-                idC ∘ (f #) ≈⟨ identityˡ ⟩
-                (f #) ≈⟨ #-Uniformity {f = f} {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]} {h = i₁} (sym inject₁) ⟩
-                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁) ∎
+                ([ idC , ((f #) +₁ h) # ] ∘ (i₁ ∘ (f #)))                ≈⟨ sym-assoc ⟩
+                (([ idC , ((f #) +₁ h) # ] ∘ i₁) ∘ (f #))                ≈⟨ ∘-resp-≈ˡ inject₁ ⟩
+                idC ∘ (f #)                                              ≈⟨ identityˡ ⟩
+                (f #)                                                    ≈⟨ #-Uniformity {f = f} {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]} {h = i₁} (sym inject₁) ⟩
+                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₁)                    ∎
             right : ∀ {X Y} {f : X ⇒ A + X} {h : Y ⇒ X + Y} 
                 → (f # +₁ h)# ∘ i₂ ≈ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂
             right {X} {Y} {f} {h} = begin 
                 (f # +₁ h)# ∘ i₂ ≈⟨ ∘-resp-≈ˡ #-Fixpoint ⟩ 
-                (([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₂) ≈⟨ assoc ⟩ 
-                ([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h) ∘ i₂) ≈⟨ ∘-resp-≈ ([]-congˡ identityˡ) +₁∘i₂ ⟩ 
-                ([ idC , ((f #) +₁ h) # ] ∘ (i₂ ∘ h)) ≈⟨ sym-assoc ⟩ 
-                ([ idC , ((f #) +₁ h) # ] ∘ i₂) ∘ h ≈⟨ ∘-resp-≈ˡ inject₂ ⟩ 
-                ((f #) +₁ h) # ∘ h ≈⟨ sym (#-Uniformity {f = ((f #) +₁ idC) ∘ h} {g = (f #) +₁ h} {h = h} (
+                (([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h)) ∘ i₂)                               ≈⟨ assoc ⟩ 
+                ([ idC , idC ∘ (((f #) +₁ h) #) ] ∘ ((f #) +₁ h) ∘ i₂)                                 ≈⟨ ∘-resp-≈ ([]-congˡ identityˡ) +₁∘i₂ ⟩ 
+                ([ idC , ((f #) +₁ h) # ] ∘ (i₂ ∘ h))                                                  ≈⟨ sym-assoc ⟩ 
+                ([ idC , ((f #) +₁ h) # ] ∘ i₂) ∘ h                                                    ≈⟨ ∘-resp-≈ˡ inject₂ ⟩ 
+                ((f #) +₁ h) # ∘ h                                                                     ≈⟨ sym (#-Uniformity {f = ((f #) +₁ idC) ∘ h} {g = (f #) +₁ h} {h = h} (
                     begin 
-                        (idC +₁ h) ∘ ((f #) +₁ idC) ∘ h ≈⟨ sym-assoc ⟩ 
+                        (idC +₁ h) ∘ ((f #) +₁ idC) ∘ h     ≈⟨ sym-assoc ⟩ 
                         (((idC +₁ h) ∘ ((f #) +₁ idC)) ∘ h) ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩ 
-                        (((idC ∘ (f #)) +₁ (h ∘ idC)) ∘ h) ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩ 
-                        (f # +₁ h) ∘ h  ∎)) ⟩ 
+                        (((idC ∘ (f #)) +₁ (h ∘ idC)) ∘ h)  ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩ 
+                        (f # +₁ h) ∘ h                      ∎)
+                    )⟩ 
                 ((((f #) +₁ idC) ∘ h) #) ≈⟨ #-Compositionality ⟩ 
                 (([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ])# ∘ i₂) ≈⟨ ∘-resp-≈ˡ (#-Uniformity {f = [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]} {g = [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]} {h = [ i₁ , h ]} (
                     begin 
-                        (idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ] ≈⟨ ∘-resp-≈ʳ ∘[] ⟩ 
-                        (idC +₁ [ i₁ , h ]) ∘ [ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ] ≈⟨ ∘-resp-≈ʳ ([]-congʳ inject₁) ⟩ 
-                        ((idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ]) ≈⟨ ∘[] ⟩ 
-                        [ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f) , (idC +₁ [ i₁ , h ]) ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h) ] ≈⟨ []-cong₂ sym-assoc sym-assoc ⟩ 
-                        [ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f , ((idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ]) ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ ∘[]) ⟩ 
+                        (idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ [ i₁ , h ]                                                                 ≈⟨ ∘-resp-≈ʳ ∘[] ⟩ 
+                        (idC +₁ [ i₁ , h ]) ∘ [ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ]                                 ≈⟨ ∘-resp-≈ʳ ([]-congʳ inject₁) ⟩ 
+                        ((idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h ])                                                  ≈⟨ ∘[] ⟩ 
+                        [ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f) , (idC +₁ [ i₁ , h ]) ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ] ∘ h) ]                          ≈⟨ []-cong₂ sym-assoc sym-assoc ⟩ 
+                        [ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f , ((idC +₁ [ i₁ , h ]) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ i₂ ]) ∘ h ]                          ≈⟨ []-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ ∘[]) ⟩ 
                         [ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f , ([ (idC +₁ [ i₁ , h ]) ∘ ((idC +₁ i₁) ∘ f) , (idC +₁ [ i₁ , h ]) ∘ (i₂ ∘ i₂) ]) ∘ h ] ≈⟨ []-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² (inject₁))) (∘-resp-≈ˡ ([]-cong₂ sym-assoc sym-assoc)) ⟩ 
-                        [ (idC +₁ i₁) ∘ f , ([ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f , ((idC +₁ [ i₁ , h ]) ∘ i₂) ∘ i₂ ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ inject₂))) ⟩ 
-                        [ (idC +₁ i₁) ∘ f , ([ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f , (i₂ ∘ [ i₁ , h ]) ∘ i₂ ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁)) assoc)) ⟩ 
-                        [ (idC +₁ i₁) ∘ f , ([ (idC +₁ i₁) ∘ f , i₂ ∘ ([ i₁ , h ] ∘ i₂) ]) ∘ h ] ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-congˡ (∘-resp-≈ʳ inject₂))) ⟩ 
-                        [ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ []-congʳ (sym (inject₁)) ⟩ 
-                        [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ] ≈⟨ sym ∘[] ⟩ 
-                        [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ] ∎)) ⟩ 
-                (([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ]) ∘ i₂) ≈⟨ assoc ⟩ 
-                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ ([ i₁ , h ] ∘ i₂)) ≈⟨ (∘-resp-≈ʳ $ inject₂) ⟩ 
-                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h) ≈⟨ sym $ ∘-resp-≈ˡ inject₂ ⟩ 
-                (([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂) ∘ h) ≈⟨ assoc ⟩ 
-                ([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂ ∘ h) ≈⟨ sym (∘-resp-≈ ([]-congˡ identityˡ) inject₂) ⟩ 
+                        [ (idC +₁ i₁) ∘ f , ([ ((idC +₁ [ i₁ , h ]) ∘ (idC +₁ i₁)) ∘ f , ((idC +₁ [ i₁ , h ]) ∘ i₂) ∘ i₂ ]) ∘ h ]                        ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ inject₂))) ⟩ 
+                        [ (idC +₁ i₁) ∘ f , ([ ((idC ∘ idC) +₁ ([ i₁ , h ] ∘ i₁)) ∘ f , (i₂ ∘ [ i₁ , h ]) ∘ i₂ ]) ∘ h ]                                  ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identity² inject₁)) assoc)) ⟩ 
+                        [ (idC +₁ i₁) ∘ f , ([ (idC +₁ i₁) ∘ f , i₂ ∘ ([ i₁ , h ] ∘ i₂) ]) ∘ h ]                                                         ≈⟨ []-congˡ (∘-resp-≈ˡ ([]-congˡ (∘-resp-≈ʳ inject₂))) ⟩ 
+                        [ (idC +₁ i₁) ∘ f , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ]                                                                           ≈⟨ []-congʳ (sym (inject₁)) ⟩ 
+                        [ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₁ , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ h ]                                                         ≈⟨ sym ∘[] ⟩ 
+                        [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ [ i₁ , h ]                                                                                        ∎)
+                    )⟩ 
+                (([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ [ i₁ , h ]) ∘ i₂)                                   ≈⟨ assoc ⟩ 
+                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ ([ i₁ , h ] ∘ i₂))                                   ≈⟨ (∘-resp-≈ʳ $ inject₂) ⟩ 
+                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ h)                                                   ≈⟨ sym $ ∘-resp-≈ˡ inject₂ ⟩ 
+                (([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂) ∘ h)                                  ≈⟨ assoc ⟩ 
+                ([ idC , [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ i₂ ∘ h)                                    ≈⟨ sym (∘-resp-≈ ([]-congˡ identityˡ) inject₂) ⟩ 
                 ([ idC , idC ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] ∘ i₂)) ≈⟨ sym-assoc ⟩ 
                 (([ idC , idC ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ] ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ]) ∘ i₂) ≈⟨ ∘-resp-≈ˡ (sym #-Fixpoint) ⟩ 
-                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂) ∎
+                ([ (idC +₁ i₁) ∘ f , i₂ ∘ h ] # ∘ i₂)                                                  ∎
 
     -- unguarded elgot-algebras are just Id-guarded Elgot-Algebras
     Unguarded↔Id-Guarded : ((ea : Elgot-Algebra) → Guarded-Elgot-Algebra (Id-Algebra (Elgot-Algebra.A ea))) ∧ (∀ {A : Obj} → Guarded-Elgot-Algebra (Id-Algebra A) → Elgot-Algebra)
diff --git a/ElgotAlgebras.agda b/ElgotAlgebras.agda
index d5daf7b..10e4f2e 100644
--- a/ElgotAlgebras.agda
+++ b/ElgotAlgebras.agda
@@ -43,15 +43,15 @@ module _ (CC : CocartesianCategory o ℓ e) where
         ; _≈_       = λ f g → Elgot-Algebra-Morphism.h f ≈ Elgot-Algebra-Morphism.h g
         ; id        = λ {EB} → let open Elgot-Algebra EB in 
                         record { h = idC; preserves = λ {X : Obj} {f : X ⇒ A + X} → begin 
-                            idC ∘ f # ≈⟨ identityˡ ⟩ 
-                            (f #) ≈⟨ sym $ #-resp-≈ identityˡ ⟩ 
-                            ((idC ∘ f) #) ≈⟨ sym (#-resp-≈ (∘-resp-≈ˡ +-η)) ⟩ 
-                            (([ i₁ , i₂ ] ∘ f)#) ≈⟨ sym $ #-resp-≈ (∘-resp-≈ˡ ([]-cong₂ identityʳ identityʳ)) ⟩ 
-                            (([ i₁ ∘ idC , i₂ ∘ idC ] ∘ f)#) ≈⟨ sym $ #-resp-≈ (∘-resp-≈ˡ []∘+₁) ⟩ 
+                            idC ∘ f #                             ≈⟨ identityˡ ⟩ 
+                            (f #)                                 ≈⟨ sym $ #-resp-≈ identityˡ ⟩ 
+                            ((idC ∘ f) #)                         ≈⟨ sym (#-resp-≈ (∘-resp-≈ˡ +-η)) ⟩ 
+                            (([ i₁ , i₂ ] ∘ f)#)                  ≈⟨ sym $ #-resp-≈ (∘-resp-≈ˡ ([]-cong₂ identityʳ identityʳ)) ⟩ 
+                            (([ i₁ ∘ idC , i₂ ∘ idC ] ∘ f)#)      ≈⟨ sym $ #-resp-≈ (∘-resp-≈ˡ []∘+₁) ⟩ 
                             ((([ i₁ , i₂ ] ∘ (idC +₁ idC)) ∘ f)#) ≈⟨ #-resp-≈ assoc ⟩ 
-                            (([ i₁ , i₂ ] ∘ (idC +₁ idC) ∘ f)#) ≈⟨ #-resp-≈ (∘-resp-≈ˡ +-η) ⟩
-                            ((idC ∘ (idC +₁ idC) ∘ f)#) ≈⟨ #-resp-≈ identityˡ ⟩ 
-                            ((idC +₁ idC) ∘ f) # ∎ }
+                            (([ i₁ , i₂ ] ∘ (idC +₁ idC) ∘ f)#)   ≈⟨ #-resp-≈ (∘-resp-≈ˡ +-η) ⟩
+                            ((idC ∘ (idC +₁ idC) ∘ f)#)           ≈⟨ #-resp-≈ identityˡ ⟩ 
+                            ((idC +₁ idC) ∘ f) #                  ∎ }
         ; _∘_       = λ {EA} {EB} {EC} f g → let 
                         open Elgot-Algebra-Morphism f renaming (h to hᶠ; preserves to preservesᶠ)
                         open Elgot-Algebra-Morphism g renaming (h to hᵍ; preserves to preservesᵍ)
@@ -59,13 +59,13 @@ module _ (CC : CocartesianCategory o ℓ e) where
                         open Elgot-Algebra EB using () renaming (_# to _#ᵇ; A to B)
                         open Elgot-Algebra EC using () renaming (_# to _#ᶜ; A to C; #-resp-≈ to #ᶜ-resp-≈)
                         in record { h = hᶠ ∘ hᵍ; preserves = λ {X} {f : X ⇒ A + X} → begin 
-                            (hᶠ ∘ hᵍ) ∘ (f #ᵃ) ≈⟨ assoc ⟩
-                            (hᶠ ∘ hᵍ ∘ (f #ᵃ)) ≈⟨ ∘-resp-≈ʳ preservesᵍ ⟩ 
-                            (hᶠ ∘ (((hᵍ +₁ idC) ∘ f) #ᵇ)) ≈⟨ preservesᶠ ⟩ 
-                            (((hᶠ +₁ idC) ∘ (hᵍ +₁ idC) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ sym-assoc ⟩ 
+                            (hᶠ ∘ hᵍ) ∘ (f #ᵃ)                     ≈⟨ assoc ⟩
+                            (hᶠ ∘ hᵍ ∘ (f #ᵃ))                     ≈⟨ ∘-resp-≈ʳ preservesᵍ ⟩ 
+                            (hᶠ ∘ (((hᵍ +₁ idC) ∘ f) #ᵇ))          ≈⟨ preservesᶠ ⟩ 
+                            (((hᶠ +₁ idC) ∘ (hᵍ +₁ idC) ∘ f) #ᶜ)   ≈⟨ #ᶜ-resp-≈ sym-assoc ⟩ 
                             ((((hᶠ +₁ idC) ∘ (hᵍ +₁ idC)) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ (∘-resp-≈ˡ +₁∘+₁) ⟩ 
-                            ((((hᶠ ∘ hᵍ) +₁ (idC ∘ idC)) ∘ f) #ᶜ) ≈⟨ #ᶜ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ refl (identity²))) ⟩ 
-                            ((hᶠ ∘ hᵍ +₁ idC) ∘ f) #ᶜ ∎ }
+                            ((((hᶠ ∘ hᵍ) +₁ (idC ∘ idC)) ∘ f) #ᶜ)  ≈⟨ #ᶜ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ refl (identity²))) ⟩ 
+                            ((hᶠ ∘ hᵍ +₁ idC) ∘ f) #ᶜ              ∎ }
         ; identityˡ = identityˡ
         ; identityʳ = identityʳ
         ; identity² = identity²
@@ -110,60 +110,61 @@ module _ (CC : CocartesianCategory o ℓ e) where
         { A = A×B
         ; _# = λ {X : Obj} (h : X ⇒ A×B + X) → ⟨ ((π₁ +₁ idC) ∘ h)#ᵃ , ((π₂ +₁ idC) ∘ h)#ᵇ ⟩
         ; #-Fixpoint = λ {X} {f} → begin
-            ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ ⟨⟩-cong₂ #ᵃ-Fixpoint #ᵇ-Fixpoint ⟩
+            ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩                                                             ≈⟨ ⟨⟩-cong₂ #ᵃ-Fixpoint #ᵇ-Fixpoint ⟩
             ⟨ [ idC , ((π₁ +₁ idC) ∘ f)#ᵃ ] ∘ ((π₁ +₁ idC) ∘ f) , [ idC , ((π₂ +₁ idC) ∘ f)#ᵇ ] ∘ ((π₂ +₁ idC) ∘ f) ⟩ ≈⟨ ⟨⟩-cong₂ sym-assoc sym-assoc ⟩
             ⟨ ([ idC , ((π₁ +₁ idC) ∘ f)#ᵃ ] ∘ (π₁ +₁ idC)) ∘ f , ([ idC , ((π₂ +₁ idC) ∘ f)#ᵇ ] ∘ (π₂ +₁ idC)) ∘ f ⟩ ≈⟨ ⟨⟩-cong₂ (∘-resp-≈ˡ []∘+₁) (∘-resp-≈ˡ []∘+₁) ⟩
-            ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ∘ f , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ∘ f ⟩ ≈⟨ sym ∘-distribʳ-⟨⟩ ⟩
-            (⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ∘ f) ≈⟨ ∘-resp-≈ˡ (unique′ 
+            ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ∘ f , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ∘ f ⟩           ≈⟨ sym ∘-distribʳ-⟨⟩ ⟩
+            (⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ∘ f)             ≈⟨ ∘-resp-≈ˡ (unique′ 
                 (begin 
                     π₁ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₁ ⟩ 
-                    [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] ≈⟨ []-cong₂ identityˡ identityʳ ⟩
-                    [ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ] ≈⟨ sym ([]-cong₂ identityʳ project₁) ⟩
-                    [ π₁ ∘ idC , π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ≈⟨ sym ∘[] ⟩
-                    π₁ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]  ∎) 
+                    [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ]                                                     ≈⟨ []-cong₂ identityˡ identityʳ ⟩
+                    [ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ]                                                                 ≈⟨ sym ([]-cong₂ identityʳ project₁) ⟩
+                    [ π₁ ∘ idC , π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                            ≈⟨ sym ∘[] ⟩
+                    π₁ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                                 ∎) 
                 (begin 
                     π₂ ∘ ⟨ [ idC ∘ π₁ , ((π₁ +₁ idC) ∘ f)#ᵃ ∘ idC ] , [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ⟩ ≈⟨ project₂ ⟩ 
-                    [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ] ≈⟨ []-cong₂ identityˡ identityʳ ⟩
-                    [ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ] ≈⟨ sym ([]-cong₂ identityʳ project₂) ⟩
-                    [ π₂ ∘ idC , π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ≈⟨ sym ∘[] ⟩
-                    π₂ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]  ∎) )⟩
-            ([ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∘ f) ∎
+                    [ idC ∘ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ∘ idC ]                                                     ≈⟨ []-cong₂ identityˡ identityʳ ⟩
+                    [ π₂ , ((π₂ +₁ idC) ∘ f)#ᵇ ]                                                                 ≈⟨ sym ([]-cong₂ identityʳ project₂) ⟩
+                    [ π₂ ∘ idC , π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                            ≈⟨ sym ∘[] ⟩
+                    π₂ ∘ [ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ]                                 ∎)
+                )⟩
+            ([ idC , ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ] ∘ f)                                             ∎
         ; #-Uniformity = λ {X Y f g h} uni → unique′ (
             begin 
-                π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₁ ⟩ 
-                (((π₁ +₁ idC) ∘ f)#ᵃ) ≈⟨ #ᵃ-Uniformity (
+                π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩         ≈⟨ project₁ ⟩ 
+                (((π₁ +₁ idC) ∘ f)#ᵃ)                                      ≈⟨ #ᵃ-Uniformity (
                     begin 
-                        (idC +₁ h) ∘ (π₁ +₁ idC) ∘ f ≈⟨ sym-assoc ⟩ 
+                        (idC +₁ h) ∘ (π₁ +₁ idC) ∘ f   ≈⟨ sym-assoc ⟩ 
                         ((idC +₁ h) ∘ (π₁ +₁ idC)) ∘ f ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩
-                        (idC ∘ π₁ +₁ h ∘ idC) ∘ f ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩
-                        ((π₁ +₁ h) ∘ f) ≈⟨ sym (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) ⟩
-                        (((π₁ ∘ idC +₁ idC ∘ h)) ∘ f) ≈⟨ sym (∘-resp-≈ˡ +₁∘+₁) ⟩
+                        (idC ∘ π₁ +₁ h ∘ idC) ∘ f      ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩
+                        ((π₁ +₁ h) ∘ f)                ≈⟨ sym (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) ⟩
+                        (((π₁ ∘ idC +₁ idC ∘ h)) ∘ f)  ≈⟨ sym (∘-resp-≈ˡ +₁∘+₁) ⟩
                         ((π₁ +₁ idC) ∘ (idC +₁ h)) ∘ f ≈⟨ assoc ⟩
                         (π₁ +₁ idC) ∘ ((idC +₁ h) ∘ f) ≈⟨ ∘-resp-≈ʳ uni ⟩
-                        (π₁ +₁ idC) ∘ g ∘ h ≈⟨ sym-assoc ⟩
-                        ((π₁ +₁ idC) ∘ g) ∘ h ∎
+                        (π₁ +₁ idC) ∘ g ∘ h            ≈⟨ sym-assoc ⟩
+                        ((π₁ +₁ idC) ∘ g) ∘ h          ∎
                     )⟩
-                (((π₁ +₁ idC) ∘ g)#ᵃ ∘ h) ≈⟨ sym (∘-resp-≈ˡ project₁) ⟩
+                (((π₁ +₁ idC) ∘ g)#ᵃ ∘ h)                                  ≈⟨ sym (∘-resp-≈ˡ project₁) ⟩
                 ((π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩) ∘ h) ≈⟨ assoc ⟩
-                π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h ∎
+                π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h     ∎
             ) (
             begin 
-                π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ ≈⟨ project₂ ⟩ 
+                π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩         ≈⟨ project₂ ⟩ 
                 ((π₂ +₁ idC) ∘ f)#ᵇ ≈⟨ #ᵇ-Uniformity (
                     begin 
-                        (idC +₁ h) ∘ (π₂ +₁ idC) ∘ f ≈⟨ sym-assoc ⟩
+                        (idC +₁ h) ∘ (π₂ +₁ idC) ∘ f     ≈⟨ sym-assoc ⟩
                         (((idC +₁ h) ∘ (π₂ +₁ idC)) ∘ f) ≈⟨ ∘-resp-≈ˡ +₁∘+₁ ⟩
-                        ((idC ∘ π₂ +₁ h ∘ idC) ∘ f) ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩
-                        ((π₂ +₁ h) ∘ f) ≈⟨ sym (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) ⟩
-                        ((((π₂ ∘ idC +₁ idC ∘ h)) ∘ f)) ≈⟨ sym (∘-resp-≈ˡ +₁∘+₁) ⟩
+                        ((idC ∘ π₂ +₁ h ∘ idC) ∘ f)      ≈⟨ ∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ) ⟩
+                        ((π₂ +₁ h) ∘ f)                  ≈⟨ sym (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) ⟩
+                        ((((π₂ ∘ idC +₁ idC ∘ h)) ∘ f))  ≈⟨ sym (∘-resp-≈ˡ +₁∘+₁) ⟩
                         ((π₂ +₁ idC) ∘ ((idC +₁ h))) ∘ f ≈⟨ assoc ⟩
-                        (π₂ +₁ idC) ∘ ((idC +₁ h)) ∘ f ≈⟨ ∘-resp-≈ʳ uni ⟩
-                        (π₂ +₁ idC) ∘ g ∘ h ≈⟨ sym-assoc ⟩
-                        ((π₂ +₁ idC) ∘ g) ∘ h ∎
+                        (π₂ +₁ idC) ∘ ((idC +₁ h)) ∘ f   ≈⟨ ∘-resp-≈ʳ uni ⟩
+                        (π₂ +₁ idC) ∘ g ∘ h              ≈⟨ sym-assoc ⟩
+                        ((π₂ +₁ idC) ∘ g) ∘ h            ∎
                     )⟩
                 ((π₂ +₁ idC) ∘ g)#ᵇ ∘ h ≈⟨ sym (∘-resp-≈ˡ project₂) ⟩
                 ((π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩) ∘ h) ≈⟨ assoc ⟩
-                π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h ∎
+                π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ g)#ᵃ , ((π₂ +₁ idC) ∘ g)#ᵇ ⟩ ∘ h     ∎
             )
         ; #-Folding = λ {X} {Y} {f} {h} → ⟨⟩-cong₂ (foldingˡ {X} {Y}) (foldingʳ {X} {Y})
         ; #-resp-≈ = λ fg → ⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ʳ fg)) (#ᵇ-resp-≈ (∘-resp-≈ʳ fg))
@@ -177,29 +178,29 @@ module _ (CC : CocartesianCategory o ℓ e) where
             foldingˡ : ∀ {X} {Y} {f} {h} → (((π₁ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ) ≈ ((π₁ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ
             foldingˡ {X} {Y} {f} {h} = begin 
                 ((π₁ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵃ ≈⟨ #ᵃ-resp-≈ +₁∘+₁ ⟩ 
-                ((π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ idC ∘ h)#ᵃ) ≈⟨ #ᵃ-resp-≈ (+₁-cong₂ project₁ identityˡ) ⟩ 
-                ((((π₁ +₁ idC) ∘ f)#ᵃ +₁ h)#ᵃ) ≈⟨ #ᵃ-Folding ⟩ 
-                ([ (idC +₁ i₁) ∘ ((π₁ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵃ) ≈⟨ #ᵃ-resp-≈ ([]-congʳ sym-assoc) ⟩ 
-                ([ ((idC +₁ i₁) ∘ (π₁ +₁ idC)) ∘ f , i₂ ∘ h ] #ᵃ) ≈⟨ #ᵃ-resp-≈ ([]-congʳ (∘-resp-≈ˡ +₁∘+₁)) ⟩ 
-                ([ ((idC ∘ π₁ +₁ i₁ ∘ idC)) ∘ f , i₂ ∘ h ] #ᵃ) ≈⟨ #ᵃ-resp-≈ ([]-congʳ (∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ))) ⟩ 
-                ([ ((π₁ +₁ i₁)) ∘ f , i₂ ∘ h ] #ᵃ) ≈⟨ sym (#ᵃ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) (∘-resp-≈ˡ identityʳ))) ⟩ 
-                (([ (π₁ ∘ idC +₁ idC ∘ i₁) ∘ f ,  (i₂ ∘ idC) ∘ h ])#ᵃ) ≈⟨ sym (#ᵃ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ +₁∘i₂))) ⟩ 
-                (([ ((π₁ +₁ idC) ∘ (idC +₁ i₁)) ∘ f , ((π₁ +₁ idC) ∘ i₂) ∘ h ])#ᵃ) ≈⟨ #ᵃ-resp-≈ ([]-cong₂ assoc assoc) ⟩ 
-                (([ (π₁ +₁ idC) ∘ (idC +₁ i₁) ∘ f , (π₁ +₁ idC) ∘ i₂ ∘ h ])#ᵃ) ≈⟨ sym (#ᵃ-resp-≈ ∘[]) ⟩ 
-                ((π₁ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ ∎
+                ((π₁ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ idC ∘ h)#ᵃ)    ≈⟨ #ᵃ-resp-≈ (+₁-cong₂ project₁ identityˡ) ⟩ 
+                ((((π₁ +₁ idC) ∘ f)#ᵃ +₁ h)#ᵃ)                                         ≈⟨ #ᵃ-Folding ⟩ 
+                ([ (idC +₁ i₁) ∘ ((π₁ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵃ)                      ≈⟨ #ᵃ-resp-≈ ([]-congʳ sym-assoc) ⟩ 
+                ([ ((idC +₁ i₁) ∘ (π₁ +₁ idC)) ∘ f , i₂ ∘ h ] #ᵃ)                      ≈⟨ #ᵃ-resp-≈ ([]-congʳ (∘-resp-≈ˡ +₁∘+₁)) ⟩ 
+                ([ ((idC ∘ π₁ +₁ i₁ ∘ idC)) ∘ f , i₂ ∘ h ] #ᵃ)                         ≈⟨ #ᵃ-resp-≈ ([]-congʳ (∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ))) ⟩ 
+                ([ ((π₁ +₁ i₁)) ∘ f , i₂ ∘ h ] #ᵃ)                                     ≈⟨ sym (#ᵃ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) (∘-resp-≈ˡ identityʳ))) ⟩ 
+                (([ (π₁ ∘ idC +₁ idC ∘ i₁) ∘ f ,  (i₂ ∘ idC) ∘ h ])#ᵃ)                 ≈⟨ sym (#ᵃ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ +₁∘i₂))) ⟩ 
+                (([ ((π₁ +₁ idC) ∘ (idC +₁ i₁)) ∘ f , ((π₁ +₁ idC) ∘ i₂) ∘ h ])#ᵃ)     ≈⟨ #ᵃ-resp-≈ ([]-cong₂ assoc assoc) ⟩ 
+                (([ (π₁ +₁ idC) ∘ (idC +₁ i₁) ∘ f , (π₁ +₁ idC) ∘ i₂ ∘ h ])#ᵃ)         ≈⟨ sym (#ᵃ-resp-≈ ∘[]) ⟩ 
+                ((π₁ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵃ                         ∎
             foldingʳ : ∀ {X} {Y} {f} {h} → ((π₂ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈ ((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ
             foldingʳ {X} {Y} {f} {h} = begin
                 ((π₂ +₁ idC) ∘ (⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ h))#ᵇ ≈⟨ #ᵇ-resp-≈ +₁∘+₁ ⟩
-                ((π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ idC ∘ h)#ᵇ) ≈⟨ #ᵇ-resp-≈ (+₁-cong₂ project₂ identityˡ) ⟩
-                ((((π₂ +₁ idC) ∘ f)#ᵇ +₁ h)#ᵇ) ≈⟨ #ᵇ-Folding ⟩
-                [ (idC +₁ i₁) ∘ ((π₂ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵇ ≈⟨ #ᵇ-resp-≈ ([]-congʳ sym-assoc) ⟩
-                ([ ((idC +₁ i₁) ∘ (π₂ +₁ idC)) ∘ f , i₂ ∘ h ] #ᵇ) ≈⟨ #ᵇ-resp-≈ ([]-congʳ (∘-resp-≈ˡ +₁∘+₁)) ⟩
-                ([ ((idC ∘ π₂ +₁ i₁ ∘ idC)) ∘ f , i₂ ∘ h ] #ᵇ) ≈⟨ #ᵇ-resp-≈ ([]-congʳ (∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ))) ⟩
-                ([ ((π₂ +₁ i₁)) ∘ f , i₂ ∘ h ] #ᵇ) ≈⟨ sym (#ᵇ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) (∘-resp-≈ˡ identityʳ))) ⟩
-                (([ (π₂ ∘ idC +₁ idC ∘ i₁) ∘ f , (i₂ ∘ idC) ∘ h ])#ᵇ) ≈⟨ sym (#ᵇ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ +₁∘i₂))) ⟩
-                (([ ((π₂ +₁ idC) ∘ (idC +₁ i₁)) ∘ f , ((π₂ +₁ idC) ∘ i₂) ∘ h ])#ᵇ) ≈⟨ #ᵇ-resp-≈ ([]-cong₂ assoc assoc) ⟩
-                (([ (π₂ +₁ idC) ∘ (idC +₁ i₁) ∘ f , (π₂ +₁ idC) ∘ i₂ ∘ h ])#ᵇ) ≈⟨ sym (#ᵇ-resp-≈ ∘[]) ⟩
-                ((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ ∎
+                ((π₂ ∘ ⟨ ((π₁ +₁ idC) ∘ f)#ᵃ , ((π₂ +₁ idC) ∘ f)#ᵇ ⟩ +₁ idC ∘ h)#ᵇ)    ≈⟨ #ᵇ-resp-≈ (+₁-cong₂ project₂ identityˡ) ⟩
+                ((((π₂ +₁ idC) ∘ f)#ᵇ +₁ h)#ᵇ)                                         ≈⟨ #ᵇ-Folding ⟩
+                [ (idC +₁ i₁) ∘ ((π₂ +₁ idC) ∘ f) , i₂ ∘ h ] #ᵇ                        ≈⟨ #ᵇ-resp-≈ ([]-congʳ sym-assoc) ⟩
+                ([ ((idC +₁ i₁) ∘ (π₂ +₁ idC)) ∘ f , i₂ ∘ h ] #ᵇ)                      ≈⟨ #ᵇ-resp-≈ ([]-congʳ (∘-resp-≈ˡ +₁∘+₁)) ⟩
+                ([ ((idC ∘ π₂ +₁ i₁ ∘ idC)) ∘ f , i₂ ∘ h ] #ᵇ)                         ≈⟨ #ᵇ-resp-≈ ([]-congʳ (∘-resp-≈ˡ (+₁-cong₂ identityˡ identityʳ))) ⟩
+                ([ ((π₂ +₁ i₁)) ∘ f , i₂ ∘ h ] #ᵇ)                                     ≈⟨ sym (#ᵇ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ (+₁-cong₂ identityʳ identityˡ)) (∘-resp-≈ˡ identityʳ))) ⟩
+                (([ (π₂ ∘ idC +₁ idC ∘ i₁) ∘ f , (i₂ ∘ idC) ∘ h ])#ᵇ)                  ≈⟨ sym (#ᵇ-resp-≈ ([]-cong₂ (∘-resp-≈ˡ +₁∘+₁) (∘-resp-≈ˡ +₁∘i₂))) ⟩
+                (([ ((π₂ +₁ idC) ∘ (idC +₁ i₁)) ∘ f , ((π₂ +₁ idC) ∘ i₂) ∘ h ])#ᵇ)     ≈⟨ #ᵇ-resp-≈ ([]-cong₂ assoc assoc) ⟩
+                (([ (π₂ +₁ idC) ∘ (idC +₁ i₁) ∘ f , (π₂ +₁ idC) ∘ i₂ ∘ h ])#ᵇ)         ≈⟨ sym (#ᵇ-resp-≈ ∘[]) ⟩
+                ((π₂ +₁ idC) ∘ [ (idC +₁ i₁) ∘ f , i₂ ∘ h ])#ᵇ                         ∎
 
     Product-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra CC) → Product C (Elgot-Algebra.A EA) (Elgot-Algebra.A EB) → Product Elgot-Algebras EA EB
     Product-Elgot-Algebras EA EB p = record
@@ -211,12 +212,12 @@ module _ (CC : CocartesianCategory o ℓ e) where
             open Elgot-Algebra-Morphism g renaming (h to g′; preserves to preservesᵍ)
             open Elgot-Algebra E renaming (_# to _#ᵉ) in record { h = ⟨ f′ , g′ ⟩ ; preserves = λ {X} {h} → 
                 begin 
-                    ⟨ f′ , g′ ⟩ ∘ (h #ᵉ) ≈⟨ ∘-distribʳ-⟨⟩ ⟩ 
-                    ⟨ f′ ∘ (h #ᵉ) , g′ ∘ (h #ᵉ) ⟩ ≈⟨ ⟨⟩-cong₂ preservesᶠ preservesᵍ ⟩
-                    ⟨ ((f′ +₁ idC) ∘ h) #ᵃ , ((g′ +₁ idC) ∘ h) #ᵇ ⟩ ≈⟨ sym (⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₁ identity²))) (#ᵇ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₂ identity²)))) ⟩
-                    ⟨ ((π₁ ∘ ⟨ f′ , g′ ⟩ +₁ idC ∘ idC) ∘ h) #ᵃ , ((π₂ ∘ ⟨ f′ , g′ ⟩ +₁ idC ∘ idC) ∘ h) #ᵇ ⟩ ≈⟨ sym (⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ˡ +₁∘+₁)) (#ᵇ-resp-≈ (∘-resp-≈ˡ +₁∘+₁))) ⟩
+                    ⟨ f′ , g′ ⟩ ∘ (h #ᵉ)                                                                              ≈⟨ ∘-distribʳ-⟨⟩ ⟩ 
+                    ⟨ f′ ∘ (h #ᵉ) , g′ ∘ (h #ᵉ) ⟩                                                                     ≈⟨ ⟨⟩-cong₂ preservesᶠ preservesᵍ ⟩
+                    ⟨ ((f′ +₁ idC) ∘ h) #ᵃ , ((g′ +₁ idC) ∘ h) #ᵇ ⟩                                                   ≈⟨ sym (⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₁ identity²))) (#ᵇ-resp-≈ (∘-resp-≈ˡ (+₁-cong₂ project₂ identity²)))) ⟩
+                    ⟨ ((π₁ ∘ ⟨ f′ , g′ ⟩ +₁ idC ∘ idC) ∘ h) #ᵃ , ((π₂ ∘ ⟨ f′ , g′ ⟩ +₁ idC ∘ idC) ∘ h) #ᵇ ⟩           ≈⟨ sym (⟨⟩-cong₂ (#ᵃ-resp-≈ (∘-resp-≈ˡ +₁∘+₁)) (#ᵇ-resp-≈ (∘-resp-≈ˡ +₁∘+₁))) ⟩
                     ⟨ (((π₁ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC)) ∘ h) #ᵃ , (((π₂ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC)) ∘ h) #ᵇ ⟩ ≈⟨ (⟨⟩-cong₂ (#ᵃ-resp-≈ assoc) (#ᵇ-resp-≈ assoc)) ⟩
-                    ⟨ ((π₁ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ h) #ᵃ , ((π₂ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ h) #ᵇ ⟩ ∎ }
+                    ⟨ ((π₁ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ h) #ᵃ , ((π₂ +₁ idC) ∘ (⟨ f′ , g′ ⟩ +₁ idC) ∘ h) #ᵇ ⟩     ∎ }
         ; project₁ = project₁
         ; project₂ = project₂
         ; unique = unique