minor

agda/src/Monad/Instance/K/Instance/Delay.lagda.md

@@ -109,16 +109,16 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
   now-inj {A} {x} {y} (↓≈ a∼b (now↓ x∼a) (now↓ y∼b)) = ∼-trans A x∼a (∼-trans A a∼b (∼-sym A y∼b))
 
   delayFun : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → delaySetoid A ⟶ delaySetoid B
-  delayFun {A} {B} f = record { _⟨$⟩_ = app ; cong = cong' }
+  delayFun {A} {B} f = record { _⟨$⟩_ = liftF ; cong = cong' }
     where
-      app : Delay (Setoid.Carrier A) → Delay (Setoid.Carrier B)
+      liftF : Delay (Setoid.Carrier A) → Delay (Setoid.Carrier B)
-      app (now x) = now (f ⟨$⟩ x)
+      liftF (now x) = now (f ⟨$⟩ x)
-      app (later x) = later (♯ app (♭ x))
+      liftF (later x) = later (♯ liftF (♭ x))
       -- TODO a variant of this should be useful outside
-      ↓-cong : ∀ {x : Delay (Setoid.Carrier A)} {b : Setoid.Carrier A} → _↓_ {A} x b → _↓_ {B} (app x) (f ⟨$⟩ b)
+      ↓-cong : ∀ {x : Delay (Setoid.Carrier A)} {b : Setoid.Carrier A} → _↓_ {A} x b → _↓_ {B} (liftF x) (f ⟨$⟩ b)
       ↓-cong {now x} {b} (now↓ x∼y) = now↓ (cong f x∼y) 
       ↓-cong {later x} {b} (later↓ x↓b) = later↓ (↓-cong x↓b)
-      cong' : ∀ {x y : Delay (Setoid.Carrier A)} → A [ x ≈ y ] → B [ app x ≈ app y ]
+      cong' : ∀ {x y : Delay (Setoid.Carrier A)} → A [ x ≈ y ] → B [ liftF x ≈ liftF y ]
       cong' {now x} {now y} (↓≈ a∼b (now↓ x∼a) (now↓ y∼b)) = now-cong (cong f (∼-trans A x∼a (∼-trans A a∼b (∼-sym A y∼b))))
       cong' {now x} {later y} (↓≈ a∼b (now↓ x∼a) (later↓ y↓b)) = ↓≈ (cong f (∼-trans A x∼a a∼b)) (now↓ (∼-refl B)) (later↓ (↓-cong y↓b))
       cong' {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ (cong f (∼-trans A a∼b (∼-sym A y∼b))) (later↓ (↓-cong x↓a)) (now↓ (∼-refl B))
@@ -151,6 +151,20 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
   delayFun-id {A} {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ delayFun-id (↓≈ a∼b x↓a y↓b))
   delayFun-id {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ delayFun-id (♭ x≈y))
 
+  delayFun-comp : ∀ {A B C : Setoid c (c ⊔ ℓ)} {f : A ⟶ B} {g : B ⟶ C} → delayFun (g ∘ f) ≋ (delayFun g ∘ delayFun f)
+  delayFun-comp {A} {B} {C} {f} {g} {now x} {now y} (↓≈ a∼b (now↓ x∼a) (now↓ y∼b)) = now-cong (cong g (cong f (∼-trans A x∼a (∼-trans A a∼b (∼-sym A y∼b)))))
+  delayFun-comp {A} {B} {C} {f} {g} {now x} {later y} (↓≈ a∼b (now↓ x∼a) (later↓ y↓b)) = ↓≈ (cong g (cong f (∼-trans A x∼a a∼b))) (now↓ (∼-refl C)) (later↓ (delayFun↓ g (delayFun↓ f y↓b)))
+  delayFun-comp {A} {B} {C} {f} {g} {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ (cong g (cong f (∼-trans A a∼b (∼-sym A y∼b)))) (later↓ (delayFun↓ (g ∘ f) x↓a)) (now↓ (∼-refl C))
+  delayFun-comp {A} {B} {C} {f} {g} {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ delayFun-comp (↓≈ a∼b x↓a y↓b))
+  delayFun-comp {A} {B} {C} {f} {g} {later x} {later y} (later≈ x≈y) = later≈ (♯ delayFun-comp (♭ x≈y))
+
+  delayFun-resp-≈ : ∀ {A B : Setoid c (c ⊔ ℓ)} {f g : A ⟶ B} → f ≋ g → delayFun f ≋ delayFun g
+  delayFun-resp-≈ {A} {B} {f} {g} f≋g {now x} {now y} x≈y = now-cong (f≋g (now-inj x≈y))
+  delayFun-resp-≈ {A} {B} {f} {g} f≋g {now x} {later y} (↓≈ a∼b (now↓ x∼a) (later↓ y↓b)) = ↓≈ (f≋g (∼-trans A x∼a a∼b)) (now↓ (∼-refl B)) (later↓ (delayFun↓ g y↓b))
+  delayFun-resp-≈ {A} {B} {f} {g} f≋g {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ (f≋g (∼-trans A a∼b (∼-sym A y∼b))) (later↓ (delayFun↓ f x↓a)) (now↓ (∼-refl B))
+  delayFun-resp-≈ {A} {B} {f} {g} f≋g {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ delayFun-resp-≈ f≋g (↓≈ a∼b x↓a y↓b))
+  delayFun-resp-≈ {A} {B} {f} {g} f≋g {later x} {later y} (later≈ x≈y) = later≈ (♯ delayFun-resp-≈ f≋g (♭ x≈y))
+
   η : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ delaySetoid A
   η A = record { _⟨$⟩_ = now ; cong = id λ x∼y → now-cong x∼y }
 
@@ -181,22 +195,29 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
   μ-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (μ B ∘ delayFun (delayFun f)) ≋ (delayFun f ∘ μ A)
   μ-natural {A} {B} f {now x} {now y} nx≈ny = cong (delayFun f) (now-inj nx≈ny)
   μ-natural {A} {B} f {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = later-eq (later≈ (♯ cong (delayFun f) (≈-sym (μ↓ (∼↓ (≈-trans (≈-sym a≈b) (≈-sym x≈a)) y↓b)))))
-  μ-natural {A} {B} f {later x} {now y} (↓≈ a∼b x↓a y↓b) = {!   !}
+  μ-natural {A} {B} f {later x} {now y} (↓≈ a≈b (later↓ x↓a) (now↓ y≈b)) = ≈-sym (later-eq (later≈ (♯ ≈-sym (μ↓ (∼↓ (cong (delayFun f) (≈-trans a≈b (≈-sym y≈b))) (delayFun↓ (delayFun f) x↓a))))))
-  μ-natural {A} {B} f {later x} {later y} (↓≈ a∼b x↓a y↓b) = {!   !}
+  μ-natural {A} {B} f {later x} {later y} (↓≈ a≈b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ μ-natural f (↓≈ a≈b x↓a y↓b))
   μ-natural {A} {B} f {later x} {later y} (later≈ x≈y) = later≈ (♯ μ-natural f (♭ x≈y))
 
+  μ-assoc : ∀ {A : Setoid c (c ⊔ ℓ)} → (μ A ∘ (delayFun (μ A))) ≋ (μ A ∘ μ (delaySetoid A))
+  μ-assoc {A} {now x} {now y} (↓≈ a≈b (now↓ x≈a) (now↓ y≈b)) = cong (μ A) (≈-trans x≈a (≈-trans a≈b (≈-sym y≈b)))
+  μ-assoc {A} {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = later-eq (later≈ (♯ cong (μ A) (≈-sym (μ↓ (∼↓ (≈-sym (≈-trans x≈a a≈b)) y↓b)))))
+  μ-assoc {A} {later x} {now y} (↓≈ a≈b (later↓ x↓a) (now↓ y≈b)) = ≈-sym (later-eq (later≈ (♯ {!   !}))) -- μ (now y) ≈ y ≈ lift (μ A) (♭ x) --> now y ↓ 
+  μ-assoc {A} {later x} {later y} (↓≈ a≈b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ μ-assoc (↓≈ a≈b x↓a y↓b))
+  μ-assoc {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ μ-assoc (♭ x≈y))
+
   delayMonad : Monad (Setoids c (c ⊔ ℓ))
   delayMonad = record
     { F = record
       { F₀ = delaySetoid
       ; F₁ = delayFun
       ; identity = delayFun-id
-      ; homomorphism = {!   !}
+      ; homomorphism = delayFun-comp
-      ; F-resp-≈ = {!   !}
+      ; F-resp-≈ = delayFun-resp-≈
       }
     ; η = ntHelper (record { η = η ; commute = η-natural })
     ; μ = ntHelper (record { η = μ ; commute = μ-natural })
-    ; assoc = {!   !}
+    ; assoc = μ-assoc
     ; sym-assoc = {!   !}
     ; identityˡ = {!   !}
     ; identityʳ = {!   !}