diff --git a/src/Algebra/Elgot/Properties.lagda.md b/src/Algebra/Elgot/Properties.lagda.md
index 4ef47b4..3bd934b 100644
--- a/src/Algebra/Elgot/Properties.lagda.md
+++ b/src/Algebra/Elgot/Properties.lagda.md
@@ -5,6 +5,11 @@ open import Level
 open import Category.Instance.AmbientCategory
 open import Categories.Functor
 open import Categories.Monad.Relative renaming (Monad to RMonad)
+open import Categories.Object.Initial
+open import Categories.Object.Terminal
+open import Categories.Object.NaturalNumbers.Properties.F-Algebras
+open import Categories.Functor.Algebra
+open import Categories.Functor.Coalgebra
 ```
 -->
 
@@ -24,12 +29,65 @@ module Algebra.Elgot.Properties {o ℓ e} (ambient : Ambient o ℓ e) where
   module _ {D : DelayM} (algebra : Guarded-Elgot-Algebra (DelayM.functor D)) where
     open DelayM D
     open Functor functor renaming (F₁ to D₁)
-    open RMonad kleisli
+    open RMonad kleisli using (extend)
     open Guarded-Elgot-Algebra algebra
+    open MR C
+    open M C
 
     commutes : α ∘ extend ι ≈ α ∘ (D₁ π₁)
     commutes = {!   !}
       where
         α∘ι : α ∘ ι ≈ π₁
-        α∘ι = {!   !}    
+        α∘ι = begin 
+          α ∘ ι ≈⟨ sym (IsInitial.!-unique isInitial (record { f = α ∘ ι ; commutes = begin 
+            (α ∘ ι) ∘ [ ⟨ idC , z ∘ _ ⟩ , idC ⁂ s ] ≈⟨ ∘[] ⟩ 
+            [ (α ∘ ι) ∘ ⟨ idC , z ∘ _ ⟩ , (α ∘ ι) ∘ (idC ⁂ s) ] ≈⟨ []-cong₂ helper₁ (pullʳ helper₂) ⟩ 
+            [ idC , α ∘ ι ] ≈˘⟨ {!   !} ⟩ 
+            {!   !} ≈˘⟨ {!   !} ⟩ 
+            [ idC , idC ] ∘ [ i₁ , i₂ ∘ α ∘ ι ] ∎ })) ⟩ 
+          F-Algebra-Morphism.f (IsInitial.! isInitial) ≈⟨ IsInitial.!-unique isInitial (record { f = π₁ ; commutes = begin 
+            π₁ ∘ [ ⟨ idC , z ∘ _ ⟩ , idC ⁂ s ] ≈⟨ ∘[] ⟩ 
+            [ π₁ ∘ ⟨ idC , z ∘ _ ⟩ , π₁ ∘ (idC ⁂ s) ] ≈⟨ []-cong₂ project₁ π₁∘⁂ ⟩ 
+            [ idC , idC ∘ π₁ ] ≈˘⟨ []-cong₂ inject₁ (pullˡ inject₂) ⟩ 
+            [ [ idC , idC ] ∘ i₁ , [ idC , idC ] ∘ i₂ ∘ π₁ ] ≈˘⟨ ∘[] ⟩ 
+            [ idC , idC ] ∘ [ i₁ , i₂ ∘ π₁ ] ∎ }) ⟩ 
+          π₁ ∎    
+          where
+            isInitial = PNNO⇒Initial₂ cartesianCategory coproducts ℕ A
+            helper₁ = begin 
+              (α ∘ ι) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ (sym (Terminal.!-unique (coalgebras A) (record { f = ι ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ; commutes = begin 
+                out ∘ ι ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ pullˡ ι-commutes ⟩ 
+                ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈˘⟨ refl⟩∘⟨ inject₁ ⟩ 
+                ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ pullʳ (cancelˡ (_≅_.isoʳ nno-iso)) ⟩ 
+                (idC +₁ ι) ∘ i₁ ≈⟨ +₁∘i₁ ○ identityʳ ⟩ 
+                i₁ ≈˘⟨ +₁∘i₁ ○ identityʳ ⟩ 
+                (idC +₁ ι ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩) ∘ i₁ ∎ }))) ⟩ 
+              α ∘ F-Coalgebra-Morphism.f (Terminal.! (coalgebras A)) ≈⟨ refl⟩∘⟨ (Terminal.!-unique (coalgebras A) (record { f = now ; commutes = begin 
+                out ∘ now ≈⟨ unitlaw ⟩ 
+                i₁ ≈˘⟨ +₁∘i₁ ○ identityʳ ⟩ 
+                (idC +₁ now) ∘ i₁ ∎ })) ⟩
+              α ∘ now ≈⟨ {!   !} ⟩ -- TODO elgot⇒search
+              idC ∎
+            helper₂ = begin 
+              ι ∘ (idC ⁂ s) ≈⟨ sym (Terminal.!-unique (coalgebras A) (record { f = ι ∘ (idC ⁂ s) ; commutes = begin 
+                out ∘ ι ∘ (idC ⁂ s) ≈⟨ pullˡ ι-commutes ⟩ 
+                ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (idC ⁂ s) ≈⟨ {!   !} ⟩ 
+                ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ _≅_.to nno-iso ∘ i₂ ≈⟨ {!   !} ⟩ 
+                (idC +₁ ι) ∘ i₂ ≈⟨ {!   !} ⟩ 
+                {!   !} ≈⟨ {!   !} ⟩ 
+                {!   !} ≈⟨ {!   !} ⟩ 
+                {!   !} ≈⟨ {!   !} ⟩ 
+                ((idC +₁ ι) ∘ (idC +₁ (idC ⁂ s))) ∘ _≅_.from nno-iso ≈⟨ {!   !} ⟩ 
+                (idC +₁ ι ∘ (idC ⁂ s)) ∘ _≅_.from nno-iso ∎ })) ⟩ 
+              -- TODO remove last part, iota is the final morphism...
+              F-Coalgebra-Morphism.f (Terminal.! (coalgebras A)) ≈⟨ Terminal.!-unique (coalgebras A) (record { f = ι ; commutes = begin 
+                out ∘ ι ≈⟨ ι-commutes ⟩ 
+                (idC +₁ ι) ∘ _≅_.from nno-iso ∎ }) ⟩ 
+              ι ∎
+```
+
+- For every X, a final coalgebra Y → X + H Y is a free H-guarded algebra over X.
+
+```agda
+  -- final-to-guarded : ∀ {A} → ?η
 ```
\ No newline at end of file
diff --git a/src/Monad/Instance/Delay.lagda.md b/src/Monad/Instance/Delay.lagda.md
index 3d8fa08..12e8642 100644
--- a/src/Monad/Instance/Delay.lagda.md
+++ b/src/Monad/Instance/Delay.lagda.md
@@ -105,8 +105,14 @@ At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `(Y
       nno-iso : X × N ≅ X + X × N
       nno-iso = Lambek.lambek (record { ⊥ = PNNO-Algebra cartesianCategory coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ cartesianCategory coproducts ℕ X })
 
+      ι-coalg : F-Coalgebra-Morphism (record { A = X × N ; α = _≅_.from nno-iso }) (record { A = DX ; α = out })
+      ι-coalg = ! {A = record { A = X × N ; α = _≅_.from nno-iso }}
+
       ι : X × N ⇒ DX
-      ι = u (! {A = record { A = X × N ; α = _≅_.from nno-iso }})
+      ι = u ι-coalg
+
+      ι-commutes : out ∘ ι ≈ (idC +₁ ι) ∘ _≅_.from nno-iso
+      ι-commutes = commutes ι-coalg
 ```
 
 ## Delay is a monad