work on delay example

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

@@ -0,0 +1,121 @@
+<!--
+```agda 
+{-# OPTIONS --allow-unsolved-metas --guardedness --exact-split #-}
+
+open import Level
+open import Category.Ambient using (Ambient)
+open import Categories.Category
+open import Categories.Category.Instance.Setoids
+open import Categories.Monad
+open import Categories.Category.Monoidal.Instance.Setoids
+open import Categories.Category.Cocartesian
+open import Categories.Object.Terminal
+open import Function.Equality as SΠ renaming (id to idₛ)
+import Categories.Morphism.Reasoning as MR
+open import Relation.Binary
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.Sum.Function.Setoid
+open import Data.Sum.Relation.Binary.Pointwise
+open import Data.Unit.Polymorphic using (tt; ⊤)
+open import Data.Empty.Polymorphic using (⊥)
+open import Categories.NaturalTransformation using (ntHelper)
+open import Function.Base using (id)
+import Relation.Binary.PropositionalEquality as Eq
+open Eq using (_≡_)
+open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
+open import Codata.Musical.Notation
+```
+-->
+
+```agda
+module Monad.Instance.K.Instance.Delay' {c ℓ} where
+```
+
+# Capretta's Delay Monad is an Instance of K in the Category of Setoids
+
+```agda
+  data Delay (A : Set c) : Set c where
+    now : A → Delay A
+    later : ∞ (Delay A) → Delay A
+
+  data _≈s_ {A : Setoid c ℓ} : Delay (Setoid.Carrier A) → Delay (Setoid.Carrier A) → Set (c ⊔ ℓ) where
+    now : ∀ {x y} → Setoid._≈_ A x y → (now x) ≈s (now y)
+    later : ∀ {x y : Delay (Setoid.Carrier A)} → _≈s_ {A} x y → (later (♯ x)) ≈s (later (♯ y))
+
+
+  module Equality {A : Setoid c ℓ} where
+    open Setoid A renaming (Carrier to C; _≈_ to _∼_)
+    data _≈_ : Delay C → Delay C → Set ℓ where
+      now :  ∀ {x y} → x ∼ y → (now x) ≈ (now y)
+      later : ∀ {x y} → ∞ ((♭ x) ≈ (♭ y)) → (later x) ≈ (later y)
+      laterˡ : ∀ {x y} → x ≈ (♭ y) → x ≈ later y
+      laterʳ : ∀ {x y} → (♭ x) ≈ y → later x ≈ y
+
+    ≈w-refl : (a : Delay C) → a ≈ a
+    ≈w-refl (now x) = now refl
+    ≈w-refl (later x) = later (♯ ≈w-refl (♭ x))
+
+    ≈w-sym : (a b : Delay C) → a ≈ b → b ≈ a
+    ≈w-sym .(now _) .(now _) (now eq) = now (sym eq)
+    ≈w-sym (later x) (later y) (later eq) = later (♯ (≈w-sym (♭ x) (♭ y) (♭ eq)))
+    ≈w-sym x (later y) (laterˡ eq) = laterʳ (≈w-sym x (♭ y) eq)
+    ≈w-sym (later x) y (laterʳ eq) = laterˡ (≈w-sym (♭ x) y eq)
+
+    module Trans where
+      -- TODO later-trans from stdlib https://agda.github.io/agda-stdlib/v1.7.3/Category.Monad.Partiality.html#2311
+      now-trans : ∀ {a b c} → a ≈ b → b ≈ now c → a ≈ now c
+      now-trans {now x} {now x₁} {c} (now x₂) (now x₃) = now (IsEquivalence.trans (Setoid.isEquivalence A) x₂ x₃)
+      now-trans {now x} {later x₁} {c} (laterˡ a≈b) (laterʳ b≈c) = now-trans a≈b b≈c
+      now-trans {later x} {now x₁} {c} (laterʳ a≈b) (now x₂) = laterʳ (now-trans a≈b (now x₂))
+      now-trans {later x} {later x₁} {c} (later x₂) (laterʳ b≈c) = laterʳ (now-trans (♭ x₂) b≈c)
+      now-trans {later x} {later x₁} {c} (laterˡ a≈b) (laterʳ b≈c) = now-trans a≈b b≈c
+      now-trans {later x} {later x₁} {c} (laterʳ a≈b) (laterʳ b≈c) = laterʳ (now-trans a≈b (laterʳ b≈c))
+    ≈w-trans : (a b c : Delay C) → a ≈ b → b ≈ c → a ≈ c
+    ≈w-trans (now _) (now _) (now _) (now a∼b) (now b∼c) = now (IsEquivalence.trans (Setoid.isEquivalence A) a∼b b∼c)
+    ≈w-trans (now a) (now b) (later c) (now a∼b) (laterˡ b≈c) = laterˡ (≈w-trans (now a) (now b) (♭ c) (now a∼b) b≈c)
+    ≈w-trans (now a) (later b) (now c) (laterˡ a≈b) (laterʳ b≈c) = ≈w-trans (now a) (♭ b) (now c) a≈b b≈c
+    ≈w-trans (now a) (later b) (later c) (laterˡ a≈b) (later b≈c) = laterˡ (≈w-trans (now a) (♭ b) (♭ c) a≈b (♭ b≈c))
+    ≈w-trans (now a) (later b) (later c) (laterˡ a≈b) (laterˡ b≈c) = laterˡ (≈w-trans (now a) {!   !} (♭ c) a≈b {!   !})
+    ≈w-trans (now a) (later b) (later c) (laterˡ a≈b) (laterʳ b≈c) = {!   !}
+    ≈w-trans (later x) (now x₁) (now x₂) a≈b b≈c = {!   !}
+    ≈w-trans (later x) (now x₁) (later x₂) a≈b b≈c = {!   !}
+    ≈w-trans (later x) (later x₁) (now x₂) a≈b b≈c = {!   !}
+    ≈w-trans (later x) (later x₁) (later x₂) a≈b b≈c = {!   !}
+
+
+  -- data _≈w_ {A : Setoid c ℓ} : Delay (Setoid.Carrier A) → Delay (Setoid.Carrier A) → Set ℓ where
+  --   now :  ∀ {x y} → Setoid._≈_ A x y → (now x) ≈w (now y)
+  --   later : ∀ {x y} → ∞ (_≈w_ {A} (♭ x) (♭ y)) → (later x) ≈w (later y)
+  --   laterˡ : ∀ {x y} → _≈w_ {A} x (♭ y) → x ≈w later y
+  --   laterʳ : ∀ {x y} → _≈w_ {A} (♭ x) y → later x ≈w y
+
+  -- ≈w-refl : ∀ {A : Setoid c ℓ} (a : Delay (Setoid.Carrier A)) → _≈w_ {A} a a
+  -- ≈w-refl {A} (now x) = now (IsEquivalence.refl (Setoid.isEquivalence A) {x})
+  -- ≈w-refl {A} (later x) = later (♯ ≈w-refl (♭ x))
+
+  -- ≈w-sym : ∀ {A : Setoid c ℓ} (a b : Delay (Setoid.Carrier A)) → _≈w_ {A} a b → _≈w_ {A} b a
+  -- ≈w-sym {A} .(now _) .(now _) (now eq) = now (IsEquivalence.sym (Setoid.isEquivalence A) eq)
+  -- ≈w-sym {A} (later x) (later y) (later eq) = later (♯ (≈w-sym (♭ x) (♭ y) (♭ eq)))
+  -- ≈w-sym {A} x (later y) (laterˡ eq) = laterʳ (≈w-sym x (♭ y) eq)
+  -- ≈w-sym {A} (later x) y (laterʳ eq) = laterˡ (≈w-sym (♭ x) y eq)
+
+  -- ≈w-trans : ∀ {A : Setoid c ℓ} (a b c : Delay (Setoid.Carrier A)) → _≈w_ {A} a b → _≈w_ {A} b c → _≈w_ {A} a c
+  -- ≈w-trans {A} .(now _) .(now _) .(now _) (now eq₁) (now eq₂) = now (IsEquivalence.trans (Setoid.isEquivalence A) eq₁ eq₂)
+  -- ≈w-trans {A} (now x) (now y) (later z) (now eq₁) (laterˡ eq₂) = laterˡ (≈w-trans (now x) (now y) (♭ z) (now eq₁) eq₂)
+  -- ≈w-trans {A} (later x) (later y) (later z) (later eq₁) (later eq₂) = later (♯ (≈w-trans (♭ x) (♭ y) (♭ z) (♭ eq₁) (♭ eq₂)))
+  -- ≈w-trans {A} (later x) (later y) (later z) (later eq₁) (laterˡ eq₂) = laterˡ (≈w-trans (later x) (later y) (♭ z) (later eq₁) eq₂)
+  -- -- ≈w-trans {A} .(later _) .(later _) c (later x) (laterʳ eq₂) = {!   !}
+  -- ≈w-trans {A} (later x) (later y) z (later eq₁) (laterʳ eq₂) = {!   !}
+  -- ≈w-trans {A} a .(later _) .(later _) (laterˡ eq₁) (later x) = {!   !}
+  -- ≈w-trans {A} a .(later _) .(later _) (laterˡ eq₁) (laterˡ eq₂) = {!   !}
+  -- ≈w-trans {A} a .(later _) c (laterˡ eq₁) (laterʳ eq₂) = {!   !}
+  -- ≈w-trans {A} .(later _) .(now _) .(now _) (laterʳ eq₁) (now x) = {!   !}
+  -- ≈w-trans {A} .(later _) .(later _) .(later _) (laterʳ eq₁) (later x) = {!   !}
+  -- ≈w-trans {A} .(later _) b .(later _) (laterʳ eq₁) (laterˡ eq₂) = {!   !}
+  -- ≈w-trans {A} .(later _) .(later _) c (laterʳ eq₁) (laterʳ eq₂) = {!   !}
+
+  -- delay-setoid : Setoid c ℓ → Setoid c ℓ
+  -- delay-setoid A = record { Carrier = Delay Carrier ; _≈_ = _≈w_ {A} ; isEquivalence = record { refl = λ {x} → ≈w-refl x ; sym = λ {x y} → ≈w-sym x y ; trans = {!   !} } }
+  --   where open Setoid A
+
+```