Formalized Delay monad

Monad/Instance/Delay.agda

@@ -0,0 +1,68 @@
+open import Level
+open import Categories.Category.Core
+open import Categories.Category.Distributive
+open import Categories.Category.Extensive.Bundle
+open import Categories.Category.Extensive
+open import Categories.Category.BinaryProducts
+open import Categories.Category.Cocartesian
+open import Categories.Category.Cartesian
+open import Categories.Object.Terminal
+open import Categories.Category.Construction.F-Coalgebras
+open import Categories.Functor.Coalgebra
+open import Categories.Functor
+open import Categories.Monad.Construction.Kleisli
+import Categories.Morphism as M
+import Categories.Morphism.Reasoning as MR
+
+module Monad.Instance.Delay {o ℓ e} (ED : ExtensiveDistributiveCategory o ℓ e) where
+  open ExtensiveDistributiveCategory ED renaming (U to C; id to idC)
+  open Cocartesian (Extensive.cocartesian extensive)
+  open Cartesian (ExtensiveDistributiveCategory.cartesian ED)
+  open BinaryProducts products
+
+  open M C
+  open MR C
+  open Equiv
+  open HomReasoning
+
+  -- Proposition 1
+  record DelayMonad (D : Endofunctor C) : Set (o ⊔ ℓ ⊔ e) where
+    open Functor D using () renaming (F₀ to D₀; F₁ to D₁)
+
+    field
+      now : ∀ {X} → X ⇒ D₀ X
+      later : ∀ {X} → D₀ X ⇒ D₀ X
+      isIso : ∀ {X} → IsIso [ now {X} , later {X} ]
+    
+    out : ∀ {X} → D₀ X ⇒ X + D₀ X
+    out {X} = IsIso.inv (isIso {X})
+
+    field
+      _* : ∀ {X Y} → X ⇒ D₀ Y → D₀ X ⇒ D₀ Y
+      *-law : ∀ {X Y} {f : X ⇒ D₀ Y} → out ∘ (f *) ≈ [ out ∘ f , i₂ ∘ (f *) ] ∘ out
+      *-unique : ∀ {X Y} (f : X ⇒ D₀ Y) (h : D₀ X ⇒ D₀ Y) → h ≈ f *
+      *-resp-≈ : ∀ {X Y} {f h : X ⇒ D₀ Y} → f ≈ h → f * ≈ h * 
+
+    unitLaw : ∀ {X} → out {X} ∘ now {X} ≈ i₁
+    unitLaw = begin 
+      out ∘ now ≈⟨ refl⟩∘⟨ sym inject₁ ⟩ 
+      out ∘ [ now , later ] ∘ i₁ ≈⟨ cancelˡ (IsIso.isoˡ isIso) ⟩
+      i₁ ∎
+
+    toMonad : KleisliTriple C
+    toMonad = record
+      { F₀ = D₀
+      ; unit = now
+      ; extend = _*
+      ; identityʳ = λ {X} {Y} {k} → begin 
+        k * ∘ now ≈⟨ introˡ (IsIso.isoʳ isIso) ⟩∘⟨refl ⟩ 
+        (([ now , later ] ∘ out) ∘ k *) ∘ now ≈⟨ pullʳ *-law ⟩∘⟨refl ⟩
+        ([ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitLaw) ⟩
+        [ now , later ] ∘ [ out ∘ k , i₂ ∘ (k *) ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩
+        [ now , later ] ∘ out ∘ k ≈⟨ cancelˡ (IsIso.isoʳ isIso) ⟩
+        k ∎
+      ; identityˡ = λ {X} → sym (*-unique now idC)
+      ; assoc = λ {X} {Y} {Z} {f} {g} → sym (*-unique ((g *) ∘ f) ((g *) ∘ (f *)))
+      ; sym-assoc = λ {X} {Y} {Z} {f} {g} → *-unique ((g *) ∘ f) ((g *) ∘ (f *))
+      ; extend-≈ = *-resp-≈
+      }