From 98cdfffdb9d845fb32e6e9d9dc40bad68879260b Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Tue, 12 Mar 2024 16:18:07 +0100
Subject: [PATCH] minor

---
 .../src/Monad/Instance/Setoids/Delay.lagda.md |  2 +-
 agda/src/Monad/Instance/Setoids/K.lagda.md    | 30 ++++++++-----------
 2 files changed, 14 insertions(+), 18 deletions(-)

diff --git a/agda/src/Monad/Instance/Setoids/Delay.lagda.md b/agda/src/Monad/Instance/Setoids/Delay.lagda.md
index 98aa0ef..abe7f56 100644
--- a/agda/src/Monad/Instance/Setoids/Delay.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/Delay.lagda.md
@@ -44,7 +44,7 @@ module _ (A : Set c) where
       later : Delay′ → Delay
     record Delay′ : Set c where
       coinductive
-      constructor dela
+      constructor delay
       field force : Delay
   open Delay′ public
 
diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md
index b511d27..763b5a6 100644
--- a/agda/src/Monad/Instance/Setoids/K.lagda.md
+++ b/agda/src/Monad/Instance/Setoids/K.lagda.md
@@ -115,7 +115,7 @@ Now we show that `iter` defines an Elgot algebra structure on `Delay≈`
     iter≈-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (Delay≈.₀ A ⊎ₛ X)} {x : ∣ X ∣} → [ A ][ iter {A} {X} < f > x ≈ [ Function.id , iter {A} {X} < f > ] (f ⟨$⟩ x) ]
     iter≈-fixpoint {A} {X} {f} {x} with < f > x in eqx
     ...                                   | inj₁ a = ≈-refl A
-    ...                                   | inj₂ a = ≈-trans A (≈-sym A later-self) (≈-refl A)
+    ...                                   | inj₂ a = ≈-sym A later-self
 
     -- iter satisfies the uniformity law
     iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delay≈.₀ A ⊎ₛ X)} {g : Y ⟶ (Delay≈.₀ A ⊎ₛ Y)} {h : X ⟶ Y}
@@ -335,24 +335,20 @@ Now we show that helper # is iteration preserving:
       preserves' {X} {g} {x} = ≡-trans ⟦ B ⟧ step₁ step₂
         where
         step₁ : [ ⟦ B ⟧ ][ (delay-lift≈ ∘ (iter≈ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ]
-        step₁ = ≡-trans ⟦ B ⟧ (≡-trans ⟦ B ⟧ (cong (helper #) (iter-g-var g)) (sub-step₁ (disc-dom g) {inj₂ x})) (≡-sym ⟦ B ⟧ (#-Compositionality B {f = helper} {h = disc-dom g}))
+        step₁ = ≡-trans ⟦ B ⟧ (≡-trans ⟦ B ⟧ (cong (helper #) (iter-g-var g)) (≡-sym ⟦ B ⟧ (#-Uniformity B {h = [ idₛ (Delay∼.₀ A) , iter∼ (disc-dom g) ]ₛ} (λ {y} → by-uni {y})))) (≡-sym ⟦ B ⟧ (#-Compositionality B {f = helper} {h = disc-dom g}))
           where
-          sub-step₁ : (g : ‖ X ‖ ⟶ ((Delay∼.₀ A) ⊎ₛ ‖ X ‖)) → ∀ {x} → [ ⟦ B ⟧ ][ ((helper #) ∘ [ idₛ (Delay∼.₀ A) , iter∼ g ]ₛ) ⟨$⟩ x
-            ≡ ([ [ inj₁ₛ , inj₂ₛ ∘ inj₁ₛ ]ₛ ∘ helper , inj₂ₛ ∘ inj₂ₛ ]ₛ ∘ [ inj₁ₛ , g ]ₛ) # ⟨$⟩ x ]
-          sub-step₁ g {u} = ≡-sym ⟦ B ⟧ (#-Uniformity B {h = [ idₛ (Delay∼.₀ A) , iter∼ g ]ₛ} (λ {y} → last-step {y}))
-            where
-            last-step : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ (Delay∼.₀ A) ][ [ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delay∼.₀ A) , iter∼ g ]ₛ ]ₛ ∘ [ [ inj₁ₛ , inj₂ₛ ∘ inj₁ₛ ]ₛ ∘ helper , inj₂ₛ ∘ inj₂ₛ ]ₛ ∘ [ inj₁ₛ , g ]ₛ ⟨$⟩ x ≡ (helper ∘ [ idₛ (Delay∼.₀ A) , iter∼ g ]ₛ) ⟨$⟩ x ]
-            last-step {inj₁ (now a)}   = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼.₀ A))
-            last-step {inj₁ (later a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼.₀ A))
-            last-step {inj₂ a} with g ⟨$⟩ a in eqb
-            ...                | inj₁ (now b)   = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼.₀ A))
-            ...                | inj₁ (later b) = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼.₀ A))
-            ...                | inj₂ b         = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼.₀ A))
+          by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ (Delay∼.₀ A) ][ [ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delay∼.₀ A) , iter∼ (disc-dom g) ]ₛ ]ₛ ∘ [ [ inj₁ₛ , inj₂ₛ ∘ inj₁ₛ ]ₛ ∘ helper , inj₂ₛ ∘ inj₂ₛ ]ₛ ∘ [ inj₁ₛ , (disc-dom g) ]ₛ ⟨$⟩ x ≡ (helper ∘ [ idₛ (Delay∼.₀ A) , iter∼ (disc-dom g) ]ₛ) ⟨$⟩ x ]
+          by-uni {inj₁ (now a)}   = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼.₀ A))
+          by-uni {inj₁ (later a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼.₀ A))
+          by-uni {inj₂ a} with (disc-dom g) ⟨$⟩ a in eqb
+          ...                | inj₁ (now b)   = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼.₀ A))
+          ...                | inj₁ (later b) = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼.₀ A))
+          ...                | inj₂ b         = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼.₀ A))
         step₂ : [ ⟦ B ⟧ ][ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift≈ , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ]
-        step₂ = #-Uniformity B {h = ‖‖-quote} sub-step₂
+        step₂ = #-Uniformity B {h = ‖‖-quote} by-uni
           where
-          sub-step₂ : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ X ][([ inj₁ₛ , inj₂ₛ ]ₛ ∘ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g))) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift≈ , inj₂ₛ ]ₛ ∘ g) ⟨$⟩ x ]
-          sub-step₂ {x} with g ⟨$⟩ x
+          by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ X ][([ inj₁ₛ , inj₂ₛ ]ₛ ∘ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g))) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift≈ , inj₂ₛ ]ₛ ∘ g) ⟨$⟩ x ]
+          by-uni {x} with g ⟨$⟩ x
           ... | inj₁ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
           ... | inj₂ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
     open Elgot-Algebra-Morphism using (preserves) renaming (h to <<_>>)
@@ -393,7 +389,7 @@ Only uniqueness of delaylift is left now:
         cong helper-now (later∼ eq) = inj₂ (force∼ eq)
 
         iter-id :  ∀ {x} → [ A ][ x ≈  iter≈ ([ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
-        iter-id {now x} = ≈-refl A
+        iter-id {now x}   = ≈-refl A
         iter-id {later x} = later≈ λ { .force≈ → iter-id }
 
         -- the 'meat' of this proof: