diff --git a/agda/src/Category/Construction/ElgotAlgebras.lagda.md b/agda/src/Category/Construction/ElgotAlgebras.lagda.md
index 1cf9b9b..e3f0720 100644
--- a/agda/src/Category/Construction/ElgotAlgebras.lagda.md
+++ b/agda/src/Category/Construction/ElgotAlgebras.lagda.md
@@ -370,45 +370,16 @@ module Category.Construction.ElgotAlgebras {o ℓ e} {C : Category o ℓ e} wher
       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 > ∘ ⟨ [ id , (Elgot-Algebra._# A) ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ] ∘ ((π₁ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) , [ id , (Elgot-Algebra._# B) ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ] ∘ ((π₂ +₁ id) ∘ (distributeʳ⁻¹ ∘ (g ⁂ id))) ⟩ ≈˘⟨ refl⟩∘⟨ (⟨⟩-cong₂ (Elgot-Algebra.#-Fixpoint A) (Elgot-Algebra.#-Fixpoint B)) ⟩ 
       < 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
-      -- { ⊤ = Terminal.⊤ Terminal-Elgot-Algebras
-      -- ; _×_ = λ X Y → A×B-Helper {X} {Y}
-      -- ; ! = Terminal.! Terminal-Elgot-Algebras
-      -- ; π₁ = λ {X} {Y} → Product.π₁ (Product-Elgot-Algebras X Y)
-      -- ; π₂ = λ {X} {Y} → Product.π₂ (Product-Elgot-Algebras X Y)
-      -- ; ⟨_,_⟩ = λ {X} {Y} {Z} f g → Product.⟨_,_⟩ (Product-Elgot-Algebras Y Z) f g
-      -- ; !-unique = Terminal.!-unique Terminal-Elgot-Algebras
-      -- ; π₁-comp = λ {X} {Y} {f} {Z} {g} → Product.project₁ (Product-Elgot-Algebras Y Z) {h = f} {i = g}
-      -- ; π₂-comp = λ {X} {Y} {f} {Z} {g} → Product.project₂ (Product-Elgot-Algebras Y Z) {h = f} {i = g}
-      -- ; ⟨,⟩-unique = λ {C} {A} {B} {f} {g} {h} eq₁ eq₂ → Product.unique (Product-Elgot-Algebras A B) {h = h} {i = f} {j = g} eq₁ eq₂
-      -- ; _^_ = λ A X → B^A-Helper {A} {Elgot-Algebra.A X}
-      -- ; eval = λ {A} {B} → record { h = eval′ ; preserves = λ {X} {f} → begin 
-      --   eval′ ∘ ⟨ (λg ((Elgot-Algebra._# A) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)))) , _ ⟩ ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) ⟩ 
-      --   eval′ ∘ ((λg ((Elgot-Algebra._# A) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id)))) ⁂ id) ∘ ⟨ id , _ ⟩ ≈⟨ pullˡ β′ ⟩ 
-      --   ((Elgot-Algebra._# A) ((eval′ +₁ id) ∘ distributeʳ⁻¹ ∘ ((π₁ +₁ id) ∘ f ⁂ id))) ∘ ⟨ id , _ ⟩ ≈⟨ {!   !} ⟩ 
-      --   (Elgot-Algebra._# A) ((eval′ +₁ id) ∘ f) ∎ } -- ⟨ ((π₁ +₁ id) ∘ h)#ᵃ , ((π₂ +₁ id) ∘ h)#ᵇ ⟩
-      -- ; curry = λ {C} {A} {B} f → record { h = λg (Elgot-Algebra-Morphism.h f) ; preserves = {!   !} }
-      -- ; eval-comp = λ {A} {B} {C} {f} → {!   !}
-      -- ; curry-unique = λ {A} {B} {C} {f} {g} eq → {!   !}
-      -- }
-
-    Exponential-Elgot-Algebras : ∀ (EA EB : Elgot-Algebra) → Exponential Elgot-Algebras EA EB
-    Exponential-Elgot-Algebras EA EB = record 
-      { B^A = B^A-Helper {EA} {Elgot-Algebra.A EB}
-      ; product = Product-Elgot-Algebras (B^A-Helper {EA} {Elgot-Algebra.A EB}) EA
-      ; eval = record { h = {! eval′ {Elgot-Algebra.A EB} {Elgot-Algebra.A EA}  !} ; preserves = {!   !} }
-      ; λg = {!  λ {X} prod →  !}
-      ; β = {!   !}
-      ; λ-unique = {!   !}
-      }
-      -- TODO instead show canonical ccc
+    CanonicalCartesianClosed.eval-comp cccc {A} {B} {C} {f} = β′
+    CanonicalCartesianClosed.curry-unique cccc {A} {B} {C} {f} {g} eq = λ-unique′ eq
 ```