minor

src/Monad/Instance/Delay/Commutative.lagda.md

@@ -30,15 +30,6 @@ module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D
   open import Categories.Morphism.Properties C
   open Terminal using (!; !-unique; ⊤)
 
-  -- TODO should be in agda-categories
-  Kleisli⇒Monad⇒Kleisli : ∀ (K : KleisliTriple C) {X Y} (f : X ⇒ RMonad.F₀ K Y) → RMonad.extend (Monad⇒Kleisli C (Kleisli⇒Monad C K)) f ≈ RMonad.extend K f
-  Kleisli⇒Monad⇒Kleisli K {X} {Y} f = begin 
-    extend idC ∘ extend (unit ∘ f) ≈⟨ sym k-assoc ⟩ 
-    extend (extend idC ∘ unit ∘ f) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩
-    extend (idC ∘ f)               ≈⟨ extend-≈ (identityˡ) ⟩
-    extend f                       ∎
-    where open RMonad K using (unit; extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
-
   open DelayM D
   open import Monad.Instance.Delay.Strong ambient D
   open Functor functor using () renaming (F₁ to D₁; identity to D-identity; homomorphism to D-homomorphism; F-resp-≈ to D-resp-≈)
@@ -192,7 +183,7 @@ module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D
 
           fixpoint-eq : ∀ {f : D₀ X × D₀ Y ⇒ D₀ (X × Y)} → f ≈ out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ f ] ] ∘ w → f ≈ extend [ now , f ] ∘ g
           fixpoint-eq {f} fix = begin 
-            f ≈⟨ fix ⟩ 
+            f                                                                                                                                                                       ≈⟨ fix ⟩ 
             out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ f ] ] ∘ w                                                                                                                           ≈˘⟨ refl⟩∘⟨ []-cong₂ refl (refl⟩∘⟨ ([]-cong₂ refl (pullʳ inject₂))) ⟩∘⟨refl ⟩
             out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , (▷ ∘ [ now , f ]) ∘ i₂ ] ] ∘ w                                                                                                          ≈˘⟨ refl⟩∘⟨ []-cong₂ refl (sym ∘[] ○ refl⟩∘⟨ []-cong₂ (elimˡ (extend-≈ inject₁ ○ k-identityˡ)) (pullˡ k-identityʳ)) ⟩∘⟨refl ⟩
             out⁻¹ ∘ [ idC +₁ σ , [ i₂ ∘ extend ([ now , f ] ∘ i₁) ∘ τ , i₂ ∘ extend (▷ ∘ [ now , f ]) ∘ now ∘ i₂ ] ] ∘ w                                                            ≈˘⟨ refl⟩∘⟨ []-cong₂ ([]-cong₂ (sym identityʳ) (refl⟩∘⟨ (elimˡ ((extend-≈ inject₁) ○ k-identityˡ)))) ([]-cong₂ (pullʳ (pullˡ ((sym k-assoc) ○ extend-≈ (pullˡ k-identityʳ)))) (pullʳ (pullˡ (▷∘extendʳ [ now , f ])))) ⟩∘⟨refl ⟩

src/Monad/Instance/Delay/Lemmas.lagda.md

@@ -0,0 +1,30 @@
+<!--
+```agda
+open import Level
+open import Category.Instance.AmbientCategory
+open import Categories.Functor
+open import Categories.Monad.Relative using () renaming (Monad to RMonad)
+```
+-->
+
+```agda
+module Monad.Instance.Delay.Lemmas {o ℓ e} (ambient : Ambient o ℓ e) where 
+open Ambient ambient
+open import Monad.Instance.Delay ambient
+open import Monad.Instance.Delay.Strong ambient
+open import Monad.Instance.Delay.Commutative ambient
+open M C
+```
+
+# Helper Lemmas concerning the Delay Monad
+
+```agda
+module _ (D : DelayM) where
+  open DelayM D
+  module D = Functor functor
+  open RMonad kleisli using (extend)
+  
+  
+  Lemma47 : ⟨ D.₁ π₁ , D.₁ π₂ ⟩ SectionOf {!   !}
+  Lemma47 = {!   !}
+```