diff --git a/agda/src/Monad/Instance/K/Instance/Delay.lagda.md b/agda/src/Monad/Instance/K/Instance/Delay.lagda.md index 6e4fe7b..29a9927 100644 --- a/agda/src/Monad/Instance/K/Instance/Delay.lagda.md +++ b/agda/src/Monad/Instance/K/Instance/Delay.lagda.md @@ -12,7 +12,7 @@ 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 Relation.Binary using (Setoid; IsEquivalence) open import Data.Sum using (_⊎_; inj₁; inj₂) open import Data.Sum.Function.Setoid open import Data.Sum.Relation.Binary.Pointwise @@ -24,7 +24,7 @@ import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_) open import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax) open import Codata.Musical.Notation -import Category.Monad.Partiality +-- import Category.Monad.Partiality open import Category.Ambient.Setoids ``` @@ -37,211 +37,212 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where # Capretta's Delay Monad is an Instance of K in the Category of Setoids ```agda - open Setoid using () renaming (Carrier to ∣_∣) + open Setoid using () renaming (Carrier to ∣_∣; _≈_ to [_][_≡_]) + open module eq (S : Setoid c (c ⊔ ℓ)) = IsEquivalence (Setoid.isEquivalence S) using () renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans) + + data _⊥ (A : Set c) : Set c where now : A → A ⊥ later : ∞ (A ⊥) → A ⊥ - module Equality {A : Setoid c (c ⊔ ℓ)} where - open Setoid A renaming (Carrier to C; _≈_ to _∼_) - open IsEquivalence (Setoid.isEquivalence A) renaming (refl to ∼-refl; sym to ∼-sym; trans to ∼-trans) + module StrongBisimilarity (A : Setoid c (c ⊔ ℓ)) where - data _↓_ : C ⊥ → C → Set (c ⊔ ℓ) where - now↓ : ∀ {x y} (x∼y : x ∼ y) → now x ↓ y + data _∼_ : ∣ A ∣ ⊥ → ∣ A ∣ ⊥ → Set (c ⊔ ℓ) where + now∼ : ∀ {x y : ∣ A ∣} → [ A ][ x ≡ y ] → now x ∼ now y + later∼ : ∀ {x y} → ∞ (♭ x ∼ ♭ y) → later x ∼ later y + + ∼-refl : ∀ {x} → x ∼ x + ∼-refl {now x} = now∼ (≡-refl A) + ∼-refl {later x} = later∼ (♯ ∼-refl) + + ∼-sym : ∀ {x y} → x ∼ y → y ∼ x + ∼-sym {.(now _)} {.(now _)} (now∼ x≡y) = now∼ (≡-sym A x≡y) + ∼-sym {.(later _)} {.(later _)} (later∼ x∼y) = later∼ (♯ ∼-sym (♭ x∼y)) + + ∼-trans : ∀ {x y z} → x ∼ y → y ∼ z → x ∼ z + ∼-trans {.(now _)} {.(now _)} {.(now _)} (now∼ x≡y) (now∼ y≡z) = now∼ (≡-trans A x≡y y≡z) + ∼-trans {.(later _)} {.(later _)} {.(later _)} (later∼ x∼y) (later∼ y∼z) = later∼ (♯ ∼-trans (♭ x∼y) (♭ y∼z)) + + open StrongBisimilarity renaming (_∼_ to [_][_∼_]) + + module WeakBisimilarity (A : Setoid c (c ⊔ ℓ)) where + data _↓_ : ∣ A ∣ ⊥ → ∣ A ∣ → Set (c ⊔ ℓ) where + now↓ : ∀ {x y} (x≡y : [ A ][ x ≡ y ]) → now x ↓ y later↓ : ∀ {x y} (x↓y : ♭ x ↓ y) → later x ↓ y - unique↓ : ∀ {c : C ⊥} {x y : C} → c ↓ x → c ↓ y → x ∼ y - unique↓ (now↓ eq₁) (now↓ eq₂) = ∼-trans (∼-sym eq₁) eq₂ - unique↓ (later↓ p) (later↓ q) = unique↓ p q + unique↓ : ∀ {a : ∣ A ∣ ⊥} {x y : ∣ A ∣} → a ↓ x → a ↓ y → [ A ][ x ≡ y ] + unique↓ (now↓ a≡x) (now↓ a≡y) = ≡-trans A (≡-sym A a≡x) a≡y + unique↓ (later↓ a↓x) (later↓ a↓y) = unique↓ a↓x a↓y - data _≈_ : C ⊥ → C ⊥ → Set (c ⊔ ℓ) where - ↓≈ : ∀ {x y a b} (a∼b : a ∼ b) (x↓a : x ↓ a) (y↓b : y ↓ b) → x ≈ y + data _≈_ : ∣ A ∣ ⊥ → ∣ A ∣ ⊥ → Set (c ⊔ ℓ) where + ↓≈ : ∀ {x y a b} (a≡b : [ A ][ a ≡ b ]) (x↓a : x ↓ a) (y↓b : y ↓ b) → x ≈ y later≈ : ∀ {x y} (x≈y : ∞ (♭ x ≈ ♭ y)) → later x ≈ later y ≈-refl : ∀ {x} → x ≈ x - ≈-refl {now x} = ↓≈ ∼-refl (now↓ ∼-refl) (now↓ ∼-refl) + ≈-refl {now x} = ↓≈ (≡-refl A) (now↓ (≡-refl A)) (now↓ (≡-refl A)) ≈-refl {later x} = later≈ (♯ ≈-refl) ≈-sym : ∀ {x y} → x ≈ y → y ≈ x - ≈-sym (↓≈ a∼b x↓a y↓b) = ↓≈ (∼-sym a∼b) y↓b x↓a + ≈-sym (↓≈ a≡b x↓a y↓b) = ↓≈ (≡-sym A a≡b) y↓b x↓a ≈-sym (later≈ x≈y) = later≈ (♯ ≈-sym (♭ x≈y)) - ∼↓ : ∀ {x y : C} {z : C ⊥} → x ∼ y → z ↓ x → z ↓ y - ∼↓ {x} {y} {.(now _)} x∼y (now↓ a∼x) = now↓ (∼-trans a∼x x∼y) - ∼↓ {x} {y} {.(later _)} x∼y (later↓ z↓x) = later↓ (∼↓ x∼y z↓x) + ≡↓ : ∀ {x y : ∣ A ∣} {z : ∣ A ∣ ⊥} → [ A ][ x ≡ y ] → z ↓ x → z ↓ y + ≡↓ {x} {y} {.(now _)} x≡y (now↓ a≡x) = now↓ (≡-trans A a≡x x≡y) + ≡↓ {x} {y} {.(later _)} x≡y (later↓ z↓x) = later↓ (≡↓ x≡y z↓x) - ≈↓ : ∀ {x y : C ⊥} {z : C} → x ≈ y → x ↓ z → y ↓ z - ≈↓ (↓≈ a∼b (now↓ x∼a) y↓b) (now↓ x∼z) = ∼↓ (∼-trans (∼-sym a∼b) (∼-trans (∼-sym x∼a) x∼z)) y↓b - ≈↓ (↓≈ a∼b (later↓ x↓a) y↓b) (later↓ x↓z) with unique↓ x↓a x↓z - ... | a∼z = ∼↓ (∼-trans (∼-sym a∼b) a∼z) y↓b + ≈↓ : ∀ {x y : ∣ A ∣ ⊥} {z : ∣ A ∣} → x ≈ y → x ↓ z → y ↓ z + ≈↓ (↓≈ a≡b (now↓ x≡a) y↓b) (now↓ x≡z) = ≡↓ (≡-trans A (≡-sym A a≡b) (≡-trans A (≡-sym A x≡a) x≡z)) y↓b + ≈↓ (↓≈ a≡b (later↓ x↓a) y↓b) (later↓ x↓z) with unique↓ x↓a x↓z + ... | a∼z = ≡↓ (≡-trans A (≡-sym A a≡b) a∼z) y↓b ≈↓ (later≈ x) (later↓ x↓z) = later↓ (≈↓ (♭ x) x↓z) ≈-trans : ∀ {x y z} → x ≈ y → y ≈ z → x ≈ z - ≈-trans (↓≈ a∼b x↓a y↓b) (↓≈ c∼d y↓c z↓d) with unique↓ y↓b y↓c - ... | b∼c = ↓≈ (∼-trans (∼-trans a∼b b∼c) c∼d) x↓a z↓d - ≈-trans (↓≈ a∼b z↓a (later↓ x↓b)) (later≈ x≈y) = ↓≈ a∼b z↓a (later↓ (≈↓ (♭ x≈y) x↓b)) - ≈-trans (later≈ x≈y) (↓≈ a∼b (later↓ y↓a) z↓b) = ↓≈ a∼b (later↓ (≈↓ (≈-sym (♭ x≈y)) y↓a)) z↓b + ≈-trans (↓≈ a≡b x↓a y↓b) (↓≈ c≡d y↓c z↓d) with unique↓ y↓b y↓c + ... | b≡c = ↓≈ (≡-trans A (≡-trans A a≡b b≡c) c≡d) x↓a z↓d + ≈-trans (↓≈ a≡b z↓a (later↓ x↓b)) (later≈ x≈y) = ↓≈ a≡b z↓a (later↓ (≈↓ (♭ x≈y) x↓b)) + ≈-trans (later≈ x≈y) (↓≈ a≡b (later↓ y↓a) z↓b) = ↓≈ a≡b (later↓ (≈↓ (≈-sym (♭ x≈y)) y↓a)) z↓b ≈-trans (later≈ x≈y) (later≈ y≈z) = later≈ (♯ ≈-trans (♭ x≈y) (♭ y≈z)) - -- _⊥ₛ + open WeakBisimilarity renaming (_≈_ to [_][_≈_]; _↓_ to [_][_↓_]) + + ∼⇒≈ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣ ⊥} → [ A ][ x ∼ y ] → [ A ][ x ≈ y ] + ∼⇒≈ {A} {.(now _)} {.(now _)} (now∼ a≡b) = ↓≈ a≡b (now↓ (≡-refl A)) (now↓ (≡-refl A)) + ∼⇒≈ {A} {.(later _)} {.(later _)} (later∼ x∼y) = later≈ (♯ ∼⇒≈ (♭ x∼y)) + + <_> = Π._⟨$⟩_ + _⊥ₛ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ) - _⊥ₛ A = record { Carrier = ∣ A ∣ ⊥ ; _≈_ = _≈_ ; isEquivalence = record { refl = ≈-refl ; sym = ≈-sym ; trans = ≈-trans } } - where - open Equality {A} - open Equality using (↓≈; later≈; now↓; later↓; _↓_; ≈↓; ∼↓; ≈-refl; ≈-sym; ≈-trans) + _⊥ₛ A = record { Carrier = ∣ A ∣ ⊥ ; _≈_ = [_][_≈_] A ; isEquivalence = record { refl = ≈-refl A ; sym = ≈-sym A ; trans = ≈-trans A } } - _[_≈_] : ∀ (A : Setoid c (c ⊔ ℓ)) → (x y : ∣ A ∣ ⊥) → Set (c ⊔ ℓ) - A [ x ≈ y ] = Equality._≈_ {A} x y + now-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → [ A ][ x ≡ y ] → [ A ][ now x ≈ now y ] + now-cong {A} {x} {y} x∼y = ↓≈ x∼y (now↓ (≡-refl A)) (now↓ (≡-refl A)) - _[_∼_] : ∀ (A : Setoid c (c ⊔ ℓ)) → (x y : ∣ A ∣) → Set (c ⊔ ℓ) - A [ x ∼ y ] = Setoid._≈_ A x y + now-inj : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → [ A ][ now x ≈ now y ] → [ A ][ x ≡ y ] + 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)) - ∼-refl : ∀ (A : Setoid c (c ⊔ ℓ)) {x : ∣ A ∣} → A [ x ∼ x ] - ∼-refl A = IsEquivalence.refl (Setoid.isEquivalence A) - - ∼-sym : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : ∣ A ∣} → A [ x ∼ y ] → A [ y ∼ x ] - ∼-sym A = IsEquivalence.sym (Setoid.isEquivalence A) - - ∼-trans : ∀ (A : Setoid c (c ⊔ ℓ)) {x y z : ∣ A ∣} → A [ x ∼ y ] → A [ y ∼ z ] → A [ x ∼ z ] - ∼-trans A = IsEquivalence.trans (Setoid.isEquivalence A) - - now-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → A [ x ∼ y ] → A [ now x ≈ now y ] - now-cong {A} {x} {y} x∼y = ↓≈ x∼y (now↓ (∼-refl A)) (now↓ (∼-refl A)) - - -- slightly different types than later≈ - -- TODO remove this is useless - later-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣ ⊥} → A [ x ≈ y ] → A [ later (♯ x) ≈ later (♯ y) ] - later-cong {A} {x} {y} x≈y = later≈ (♯ x≈y) - - now-inj : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → A [ now x ≈ now y ] → A [ x ∼ y ] - 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)) - - liftF : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → ∣ A ∣ ⊥ → ∣ B ∣ ⊥ - liftF f (now x) = now (f ⟨$⟩ x) + liftF : ∀ {A B : Set c} → (A → B) → A ⊥ → B ⊥ + liftF f (now x) = now (f x) liftF f (later x) = later (♯ liftF f (♭ x)) - delayFun : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → A ⊥ₛ ⟶ B ⊥ₛ - delayFun {A} {B} f = record { _⟨$⟩_ = liftF f ; cong = cong' } - where - ↓-cong : ∀ {x : ∣ A ∣ ⊥} {b : ∣ A ∣} → _↓_ {A} x b → _↓_ {B} (liftF f 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 : ∣ A ∣ ⊥} → A [ x ≈ y ] → B [ liftF f x ≈ liftF f 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)) - cong' {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ cong' (↓≈ a∼b x↓a y↓b)) - cong' {later x} {later y} (later≈ x≈y) = later≈ (♯ cong' (♭ x≈y)) + lift↓ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x : ∣ A ∣ ⊥} {b : ∣ A ∣} → [ A ][ x ↓ b ] → [ B ][ liftF (f ._⟨$⟩_) x ↓ f ⟨$⟩ b ] + lift↓ {A} {B} f {now x} {b} (now↓ x≡b) = now↓ (cong f x≡b) + lift↓ {A} {B} f {later x} {b} (later↓ x↓b) = later↓ (lift↓ f x↓b) - -- this needs polymorphic universe levels + lift-cong : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x y : ∣ A ∣ ⊥} → [ A ][ x ≈ y ] → [ B ][ liftF < f > x ≈ liftF < f > y ] + lift-cong {A} {B} f {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)))) + lift-cong {A} {B} f {now x} {later y} (↓≈ a≡b (now↓ x≡a) (later↓ y↓b)) = ↓≈ (cong f (≡-trans A x≡a a≡b)) (now↓ (≡-refl B)) (later↓ (lift↓ f y↓b)) + lift-cong {A} {B} f {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ↓≈ (cong f (≡-trans A a≡b (≡-sym A y≡b))) (later↓ (lift↓ f x↓a)) (now↓ (≡-refl B)) + lift-cong {A} {B} f {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ lift-cong f (↓≈ a≡b x↓a y↓b)) + lift-cong {A} {B} f {later x} {later y} (later≈ x≈y) = later≈ (♯ lift-cong f (♭ x≈y)) + + liftFₛ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → A ⊥ₛ ⟶ B ⊥ₛ + liftFₛ {A} {B} f = record { _⟨$⟩_ = liftF < f > ; cong = lift-cong f } + +-- -- this needs polymorphic universe levels _≋_ : ∀ {c' ℓ'} {A B : Setoid c' ℓ'} → A ⟶ B → A ⟶ B → Set (c' ⊔ ℓ') _≋_ {c'} {ℓ'} {A} {B} f g = Setoid._≈_ (A ⇨ B) f g - later-eq : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣ ⊥} → A [ later (♯ x) ≈ y ] → A [ x ≈ y ] - later-eq {A} {x} {y} (↓≈ a∼b (later↓ x↓a) y↓b) = ↓≈ a∼b x↓a y↓b - later-eq {A} {now x} {later y} (later≈ x≈y) = ↓≈ (∼-refl A) (now↓ (∼-refl A)) (later↓ (≈↓ (♭ x≈y) (now↓ (∼-refl A)))) - later-eq {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ later-eq (≈-trans (later≈ (♯ ≈-refl)) (♭ x≈y))) + later-eq : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣ ⊥} → [ A ][ later (♯ x) ≈ y ] → [ A ][ x ≈ y ] + later-eq {A} {x} {y} (↓≈ a≡b (later↓ x↓a) y↓b) = ↓≈ a≡b x↓a y↓b + later-eq {A} {now x} {later y} (later≈ x≈y) = ↓≈ (≡-refl A) (now↓ (≡-refl A)) (later↓ (≈↓ A (♭ x≈y) (now↓ (≡-refl A)))) + later-eq {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ later-eq (≈-trans A (later≈ (♯ ≈-refl A)) (♭ x≈y))) - later-self : ∀ {A : Setoid c (c ⊔ ℓ)} {x : ∣ A ∣ ⊥} → A [ x ≈ later (♯ x) ] - later-self {A} {now x} = ↓≈ (∼-refl A) (now↓ (∼-refl A)) (later↓ (now↓ (∼-refl A))) - later-self {A} {later x} = later-eq (later≈ (♯ ≈-refl)) + later-self : ∀ {A : Setoid c (c ⊔ ℓ)} {x : ∣ A ∣ ⊥} → [ A ][ x ≈ later (♯ x) ] + later-self {A} {now x} = ↓≈ (≡-refl A) (now↓ (≡-refl A)) (later↓ (now↓ (≡-refl A))) + later-self {A} {later x} = later-eq (later≈ (♯ ≈-refl A)) - delayFun↓ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x : ∣ A ∣ ⊥} {y : ∣ A ∣} → _↓_ {A} x y → _↓_ {B} (delayFun f ⟨$⟩ x) (f ⟨$⟩ y) - delayFun↓ {A} {B} f {now x} {y} (now↓ x∼y) = now↓ (cong f x∼y) - delayFun↓ {A} {B} f {later x} {y} (later↓ x↓y) = later↓ (delayFun↓ f x↓y) + lift-id : ∀ {A : Setoid c (c ⊔ ℓ)} → (liftFₛ idₛ) ≋ (idₛ {A = A ⊥ₛ}) + lift-id {A} {now x} {now y} (↓≈ a≡b (now↓ x≡a) (now↓ y≡b)) = ↓≈ a≡b (now↓ x≡a) (now↓ y≡b) + lift-id {A} {now x} {later y} x≈y = x≈y + lift-id {A} {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ↓≈ a≡b (later↓ (lift↓ idₛ x↓a)) (now↓ y≡b) + lift-id {A} {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ lift-id (↓≈ a≡b x↓a y↓b)) + lift-id {A} {later x} {later y} (later≈ x≈y) = later≈ (♯ lift-id (♭ x≈y)) - delayFun-id : ∀ {A : Setoid c (c ⊔ ℓ)} → (delayFun idₛ) ≋ (idₛ {A = A ⊥ₛ}) - delayFun-id {A} {now x} {now y} (↓≈ a∼b (now↓ x∼a) (now↓ y∼b)) = ↓≈ a∼b (now↓ x∼a) (now↓ y∼b) - delayFun-id {A} {now x} {later y} x≈y = x≈y - delayFun-id {A} {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ a∼b (later↓ (delayFun↓ idₛ x↓a)) (now↓ y∼b) - 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)) + lift-comp : ∀ {A B C : Setoid c (c ⊔ ℓ)} {f : A ⟶ B} {g : B ⟶ C} → liftFₛ (g ∘ f) ≋ (liftFₛ g ∘ liftFₛ f) + lift-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))))) + lift-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↓ (lift↓ g (lift↓ f y↓b))) + lift-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↓ (lift↓ (g ∘ f) x↓a)) (now↓ (≡-refl C)) + lift-comp {A} {B} {C} {f} {g} {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ lift-comp {A} {B} {C} {f} {g} (↓≈ a≡b x↓a y↓b)) + lift-comp {A} {B} {C} {f} {g} {later x} {later y} (later≈ x≈y) = later≈ (♯ lift-comp {A} {B} {C} {f} {g} (♭ 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)) + lift-resp-≈ : ∀ {A B : Setoid c (c ⊔ ℓ)} {f g : A ⟶ B} → f ≋ g → liftFₛ f ≋ liftFₛ g + lift-resp-≈ {A} {B} {f} {g} f≋g {now x} {now y} x≈y = now-cong (f≋g (now-inj x≈y)) + lift-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↓ (lift↓ g y↓b)) + lift-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↓ (lift↓ f x↓a)) (now↓ (≡-refl B)) + lift-resp-≈ {A} {B} {f} {g} f≋g {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ lift-resp-≈ {A} {B} {f} {g} f≋g (↓≈ a≡b x↓a y↓b)) + lift-resp-≈ {A} {B} {f} {g} f≋g {later x} {later y} (later≈ x≈y) = later≈ (♯ lift-resp-≈ {A} {B} {f} {g} f≋g (♭ x≈y)) η : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ A ⊥ₛ - η A = record { _⟨$⟩_ = now ; cong = id λ x∼y → now-cong x∼y } + η A = record { _⟨$⟩_ = now ; cong = id λ x≡y → now-cong x≡y } - η↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → A [ x ∼ y ] → _↓_ {A} ((η A) ⟨$⟩ x) y - η↓ {A} {x} {y} x∼y = now↓ x∼y + η↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : ∣ A ∣} → [ A ][ x ≡ y ] → [ A ][ ((η A) ⟨$⟩ x) ↓ y ] + η↓ {A} {x} {y} x≡y = now↓ x≡y - η-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (η B ∘ f) ≋ (delayFun f ∘ η A) + η-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (η B ∘ f) ≋ (liftFₛ f ∘ η A) η-natural {A} {B} f {x} {y} x≈y = now-cong (cong f x≈y) - private - μ' : ∀ {A : Setoid c (c ⊔ ℓ)} → ∣ (A ⊥ₛ) ⊥ₛ ∣ → ∣ (A ⊥ₛ) ∣ - μ' {A} (now x) = x - μ' {A} (later x) = later (♯ μ' {A} (♭ x)) + μ : ∀ {A : Setoid c (c ⊔ ℓ)} → ∣ (A ⊥ₛ) ⊥ₛ ∣ → ∣ (A ⊥ₛ) ∣ + μ {A} (now x) = x + μ {A} (later x) = later (♯ μ {A} (♭ x)) - μ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} → _↓_ {A ⊥ₛ} x y → A [ (μ' {A} x) ≈ y ] - μ↓ {A} {now x} {y} (now↓ x≈y) = x≈y - μ↓ {A} {later x} {y} (later↓ x↓y) = ≈-trans (later≈ (♯ μ↓ x↓y)) (≈-sym later-self) + μ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} → [ A ⊥ₛ ][ x ↓ y ] → [ A ][ (μ {A} x) ≈ y ] + μ↓ {A} {now x} {y} (now↓ x≈y) = x≈y + μ↓ {A} {later x} {y} (later↓ x↓y) = ≈-trans A (later≈ (♯ μ↓ x↓y)) (≈-sym A later-self) - -- TODO do delayFun and η in the same style as μ - - μ : ∀ (A : Setoid c (c ⊔ ℓ)) → (A ⊥ₛ) ⊥ₛ ⟶ A ⊥ₛ - μ A = record { _⟨$⟩_ = μ' {A} ; cong = cong' } - where - cong' : ∀ {x y : (∣ A ∣ ⊥) ⊥} → (A ⊥ₛ) [ x ≈ y ] → A [ μ' {A} x ≈ μ' {A} y ] - cong' {x} {now y} (↓≈ a≈b x↓a (now↓ y≈b)) = μ↓ (∼↓ (≈-trans a≈b (≈-sym y≈b)) x↓a) - cong' {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = ≈-sym (μ↓ (∼↓ (≈-trans (≈-sym a≈b) (≈-sym x≈a)) (later↓ y↓b))) - cong' {later x} {later y} (↓≈ a≈b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ cong' (↓≈ a≈b x↓a y↓b)) - cong' {later x} {later y} (later≈ x≈y) = later≈ (♯ cong' (♭ x≈y)) + μ-cong : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : (∣ A ∣ ⊥) ⊥} → [ A ⊥ₛ ][ x ≈ y ] → [ A ][ μ {A} x ≈ μ {A} y ] + μ-cong A {x} {now y} (↓≈ a≈b x↓a (now↓ y≈b)) = μ↓ (≡↓ (A ⊥ₛ) (≈-trans A a≈b (≈-sym A y≈b)) x↓a) + μ-cong A {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = ≈-sym A (μ↓ (≡↓ (A ⊥ₛ) (≈-trans A (≈-sym A a≈b) (≈-sym A x≈a)) (later↓ y↓b))) + μ-cong A {later x} {later y} (↓≈ a≈b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ μ-cong A (↓≈ a≈b x↓a y↓b)) + μ-cong A {later x} {later y} (later≈ x≈y) = later≈ (♯ μ-cong A (♭ x≈y)) + + μₛ : ∀ (A : Setoid c (c ⊔ ℓ)) → (A ⊥ₛ) ⊥ₛ ⟶ A ⊥ₛ + μₛ A = record { _⟨$⟩_ = μ {A} ; cong = μ-cong A } - μ-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 (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 : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (μₛ B ∘ liftFₛ (liftFₛ f)) ≋ (liftFₛ f ∘ μₛ A) + μ-natural {A} {B} f {now x} {now y} nx≈ny = cong (liftFₛ 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 (liftFₛ f) (≈-sym A (μ↓ (≡↓ (A ⊥ₛ) (≈-trans A (≈-sym A a≈b) (≈-sym A x≈a)) y↓b))))) + μ-natural {A} {B} f {later x} {now y} (↓≈ a≈b (later↓ x↓a) (now↓ y≈b)) = ≈-sym B (later-eq (later≈ (♯ ≈-sym B (μ↓ (≡↓ (B ⊥ₛ) (cong (liftFₛ f) (≈-trans A a≈b (≈-sym A y≈b))) (lift↓ (liftFₛ f) x↓a)))))) μ-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 ⊔ ℓ)} {x : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} → _↓_ {A ⊥ₛ} x y → A [ (μ A) ⟨$⟩ x ≈ y ] + μ-assoc↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} → [ A ⊥ₛ ][ x ↓ y ] → [ A ][ (μₛ A) ⟨$⟩ x ≈ y ] μ-assoc↓ {A} {now x} {y} (now↓ x≈y) = x≈y - μ-assoc↓ {A} {later x} {y} (later↓ x↓y) = ≈-sym (later-eq (later≈ (♯ ≈-sym (μ-assoc↓ x↓y)))) + μ-assoc↓ {A} {later x} {y} (later↓ x↓y) = ≈-sym A (later-eq (later≈ (♯ ≈-sym A (μ-assoc↓ x↓y)))) - - -- TODO needs another μ↓-trans for when multiple μ's are concerned, i.e. a chain with 3 conditions... - μ↓-trans : ∀ {A : Setoid c (c ⊔ ℓ)} {x : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} {z : ∣ A ∣} → _↓_ {A ⊥ₛ} x y → _↓_ {A} y z → _↓_ {A} (μ A ⟨$⟩ x) z - μ↓-trans {A} {now x} {y} {z} (now↓ x≈y) y↓z = ≈↓ (≈-sym x≈y) y↓z + μ↓-trans : ∀ {A : Setoid c (c ⊔ ℓ)} {x : (∣ A ∣ ⊥) ⊥} {y : ∣ A ∣ ⊥} {z : ∣ A ∣} → [ A ⊥ₛ ][ x ↓ y ] → [ A ][ y ↓ z ] → [ A ][ (μₛ A ⟨$⟩ x) ↓ z ] + μ↓-trans {A} {now x} {y} {z} (now↓ x≈y) y↓z = ≈↓ A (≈-sym A x≈y) y↓z μ↓-trans {A} {later x} {y} {z} (later↓ x↓y) y↓z = later↓ (μ↓-trans x↓y y↓z) - -- μ↓-trans² : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (∣ A ∣ ⊥))} {y : Delay (∣ A ∣ ⊥)} {z : ∣ A ∣ ⊥} → _↓_ {delaySetoid (A ⊥ₛ)} x y → _↓_ {A ⊥ₛ} y z → _↓_ {A ⊥ₛ} ((delayFun (μ A)) ⟨$⟩ x) z - -- μ↓-trans² {A} {now x} {y} {now x₁} (now↓ x∼y) y↓z = now↓ (↓≈ {! !} (μ↓-trans {! !} {! y↓z !}) (now↓ (∼-refl A))) - -- μ↓-trans² {A} {now x} {y} {later x₁} (now↓ x∼y) y↓z = now↓ (↓≈ {! !} {! !} {! !}) - -- μ↓-trans² {A} {later x} {y} {z} x↓y y↓z = {! !} +-- -- μ↓-trans² : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (∣ A ∣ ⊥))} {y : Delay (∣ A ∣ ⊥)} {z : ∣ A ∣ ⊥} → _↓_ {delaySetoid (A ⊥ₛ)} x y → _↓_ {A ⊥ₛ} y z → _↓_ {A ⊥ₛ} ((delayFun (μ A)) ⟨$⟩ x) z +-- -- μ↓-trans² {A} {now x} {y} {now x₁} (now↓ x∼y) y↓z = now↓ (↓≈ {! !} (μ↓-trans {! !} {! y↓z !}) (now↓ (∼-refl A))) +-- -- μ↓-trans² {A} {now x} {y} {later x₁} (now↓ x∼y) y↓z = now↓ (↓≈ {! !} {! !} {! !}) +-- -- μ↓-trans² {A} {later x} {y} {z} x↓y y↓z = {! !} + μ-assoc' : ∀ {A : Setoid c (c ⊔ ℓ)} {x : ((∣ A ∣ ⊥)⊥)⊥} → [ A ][ (μₛ A ∘ (liftFₛ (μₛ A))) ⟨$⟩ x ∼ (μₛ A ∘ μₛ (A ⊥ₛ)) ⟨$⟩ x ] + μ-assoc' {A} {now x} = ∼-refl A + μ-assoc' {A} {later x} = later∼ (♯ μ-assoc' {A} {♭ x}) - μ-assoc : ∀ {A : Setoid c (c ⊔ ℓ)} → (μ A ∘ (delayFun (μ A))) ≋ (μ A ∘ μ (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))))) -- y , liftF (μ A) (♭ x) - μ-assoc {A} {later x} {now y} (↓≈ {_} {_} {a} {b} (↓≈ c≈d a↓c b↓d) (later↓ x↓a) (now↓ y≈b)) = ≈-sym (later-eq (later≈ (♯ cong (μ A) {y} {liftF (μ A) (♭ x)} (↓≈ (≈-sym c≈d) (≈↓ (≈-sym y≈b) b↓d) {! delayFun↓ (μ A) {♭ x} x↓a !})))) -- (↓≈ (≈-sym c≈d) (≈↓ (≈-sym y≈b) b↓d) (μ↓-trans {! x↓a !} a↓c)) - μ-assoc {A} {later x} {now y} (↓≈ (later≈ x≈y) (later↓ x↓a) (now↓ y≈b)) = {! !} - μ-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)) + -- TODO μ-assoc follows from this!! - identityˡ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : ∣ A ∣ ⊥} {y : ∣ A ∣} → _↓_ {A} x y → _↓_ {A} ((μ A) ⟨$⟩ ((delayFun (η A)) ⟨$⟩ x)) y +-- μ-assoc : ∀ {A : Setoid c (c ⊔ ℓ)} → (μ A ∘ (delayFun (μ A))) ≋ (μ A ∘ μ (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))))) -- y , liftF (μ A) (♭ x) +-- μ-assoc {A} {later x} {now y} (↓≈ {_} {_} {a} {b} (↓≈ c≈d a↓c b↓d) (later↓ x↓a) (now↓ y≈b)) = ≈-sym (later-eq (later≈ (♯ cong (μ A) {y} {liftF (μ A) (♭ x)} (↓≈ (≈-sym c≈d) (≈↓ (≈-sym y≈b) b↓d) {! delayFun↓ (μ A) {♭ x} x↓a !})))) -- (↓≈ (≈-sym c≈d) (≈↓ (≈-sym y≈b) b↓d) (μ↓-trans {! x↓a !} a↓c)) +-- μ-assoc {A} {later x} {now y} (↓≈ (later≈ x≈y) (later↓ x↓a) (now↓ y≈b)) = {! !} +-- μ-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)) + + identityˡ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : ∣ A ∣ ⊥} {y : ∣ A ∣} → [ A ][ x ↓ y ] → [ A ][ ((μₛ A) ⟨$⟩ ((liftFₛ (η A)) ⟨$⟩ x)) ↓ y ] identityˡ↓ {A} {now x} {y} x↓y = x↓y identityˡ↓ {A} {later x} {y} (later↓ x↓y) = later↓ (identityˡ↓ x↓y) - identityˡ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μ A ∘ delayFun (η A)) ≋ idₛ + identityˡ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ liftFₛ (η A)) ≋ idₛ identityˡ {A} {now x} {y} x≈y = x≈y - identityˡ {A} {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ (∼-refl A) (later↓ (identityˡ↓ x↓a)) (now↓ (∼-trans A y∼b (∼-sym A a∼b))) + identityˡ {A} {later x} {now y} (↓≈ a∼b (later↓ x↓a) (now↓ y∼b)) = ↓≈ (≡-refl A) (later↓ (identityˡ↓ x↓a)) (now↓ (≡-trans A y∼b (≡-sym A a∼b))) identityˡ {A} {later x} {later y} (↓≈ a∼b (later↓ x↓a) (later↓ y↓b)) = later≈ (♯ identityˡ (↓≈ a∼b x↓a y↓b)) identityˡ {A} {later x} {.(later _)} (later≈ x≈y) = later≈ (♯ identityˡ (♭ x≈y)) - identityʳ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μ A ∘ η (A ⊥ₛ)) ≋ idₛ + identityʳ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ η (A ⊥ₛ)) ≋ idₛ identityʳ {A} {now x} {y} x≈y = x≈y identityʳ {A} {later x} {y} x≈y = x≈y @@ -249,14 +250,14 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where delayMonad = record { F = record { F₀ = _⊥ₛ - ; F₁ = delayFun - ; identity = delayFun-id - ; homomorphism = delayFun-comp - ; F-resp-≈ = delayFun-resp-≈ + ; F₁ = liftFₛ + ; identity = lift-id + ; homomorphism = λ {X} {Y} {Z} {f} {g} → lift-comp {X} {Y} {Z} {f} {g} + ; F-resp-≈ = λ {A} {B} {f} {g} → lift-resp-≈ {A} {B} {f} {g} } ; η = ntHelper (record { η = η ; commute = η-natural }) - ; μ = ntHelper (record { η = μ ; commute = μ-natural }) - ; assoc = μ-assoc + ; μ = ntHelper (record { η = μₛ ; commute = μ-natural }) + ; assoc = {! !} ; sym-assoc = {! !} ; identityˡ = identityˡ ; identityʳ = identityʳ