From 86e45d7b71e59dfe616b75f8a0ce8ad1962b6016 Mon Sep 17 00:00:00 2001
From: Leon Vatthauer <leon.vatthauer@fau.de>
Date: Thu, 1 Feb 2024 12:51:13 +0100
Subject: [PATCH] minor

---
 .../Construction/ElgotAlgebras.lagda.md        | 18 +++++++++++-------
 1 file changed, 11 insertions(+), 7 deletions(-)

diff --git a/agda/src/Category/Construction/ElgotAlgebras.lagda.md b/agda/src/Category/Construction/ElgotAlgebras.lagda.md
index fc88e9d..1cf9b9b 100644
--- a/agda/src/Category/Construction/ElgotAlgebras.lagda.md
+++ b/agda/src/Category/Construction/ElgotAlgebras.lagda.md
@@ -366,13 +366,17 @@ module Category.Construction.ElgotAlgebras {o ℓ e} {C : Category o ℓ e} wher
             ((i₂ ∘ id) ∘ (id ⁂ id)) ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ≈⟨ (cancelʳ (identityˡ ○ ⟨⟩-unique id-comm id-comm)) ⟩∘⟨refl ⟩ 
             i₂ ∘ ⟨ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ f) ⟩ ∎
     Elgot-Algebra-Morphism.h (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) = λg < f >
-    Elgot-Algebra-Morphism.preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = begin 
-      λg < f > ∘ (Elgot-Algebra._# A) g ≈⟨ {!   !} ⟩ 
-      {!   !} ≈⟨ {!   !} ⟩
-      {!   !} ≈⟨ {!   !} ⟩
-      {!   !} ≈⟨ {!   !} ⟩
-      {!   !} ≈⟨ {!   !} ⟩
-      λg ((Elgot-Algebra._# C) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id))) ∎
+    Elgot-Algebra-Morphism.preserves (CanonicalCartesianClosed.curry cccc {A} {B} {C} f) {X} {g} = λ-unique′ (begin 
+      eval′ ∘ ((λg < f > ∘ (Elgot-Algebra._# A) g) ⁂ id) ≈⟨ refl⟩∘⟨ ⁂-cong₂ subst refl ⟩ 
+      eval′ ∘ ((λg (< f > ∘ (((Elgot-Algebra._# A) g) ⁂ id))) ⁂ id) ≈⟨ β′ ⟩ 
+      < f > ∘ (((Elgot-Algebra._# A) g) ⁂ id) ≈⟨ {!   !} ⟩ 
+      {!   !} ≈⟨ {!   !} ⟩ 
+      {!   !} ≈⟨ {!   !} ⟩ 
+      < f > ∘ ⟨ (Elgot-Algebra._# A) ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ⟩ ≈⟨ Elgot-Algebra-Morphism.preserves f ⟩ 
+      (Elgot-Algebra._# C) ((< f > +₁ id) ∘ distributeʳ⁻¹ ∘ (g ⁂ id)) ≈˘⟨ {!   !} ⟩ 
+      (Elgot-Algebra._# C) ((eval′ +₁ id) ∘ (((λg < f > ⁂ id) +₁ (id ⁂ id)) ∘ distributeʳ⁻¹) ∘ (g ⁂ id)) ≈˘⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (pullˡ (sym (distributeʳ⁻¹-natural id (λg < f >) id)))) ⟩ 
+      (Elgot-Algebra._# C) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((λg < f > +₁ id) ⁂ id) ∘ (g ⁂ id)) ≈⟨ Elgot-Algebra.#-resp-≈ C (refl⟩∘⟨ (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ refl identity²))) ⟩ 
+      (Elgot-Algebra._# C) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ (((λg < f > +₁ id) ∘ g) ⁂ id)) ∎)
     CanonicalCartesianClosed.eval-comp cccc {A} {B} {C} {f} = {!   !}
     CanonicalCartesianClosed.curry-unique cccc {A} {B} {C} {f} {g} eq = {!   !}
       -- record