From 1e7e156f0b7d6f8c98e70a4368d70d4bbde4cf8f Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Sun, 3 Dec 2023 22:12:53 +0100 Subject: [PATCH] work on delay example --- src/Monad/Instance/K/Instance/Delay'.lagda.md | 121 ++++++++++++++++++ 1 file changed, 121 insertions(+) create mode 100644 src/Monad/Instance/K/Instance/Delay'.lagda.md diff --git a/src/Monad/Instance/K/Instance/Delay'.lagda.md b/src/Monad/Instance/K/Instance/Delay'.lagda.md new file mode 100644 index 0000000..f6ace49 --- /dev/null +++ b/src/Monad/Instance/K/Instance/Delay'.lagda.md @@ -0,0 +1,121 @@ + + +```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 + +``` \ No newline at end of file