From d0e11e8142fd17565fdae7d2fdb93f3a8fa2a265 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Fri, 1 Dec 2023 20:46:12 +0100 Subject: [PATCH] work on examples --- src/Monad/Instance/K/Instance/Delay.lagda.md | 142 +++++++++++++++++++ src/Monad/Instance/K/Instance/Maybe.lagda.md | 2 - 2 files changed, 142 insertions(+), 2 deletions(-) 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..e5144cc --- /dev/null +++ b/src/Monad/Instance/K/Instance/Delay.lagda.md @@ -0,0 +1,142 @@ + + +```agda +module Monad.Instance.K.Instance.Delay {c ℓ} where +``` + +# Capretta's Delay Monad is an Instance of K in the Category of Setoids + +```agda + record Delay (A : Set c) : Set c where + coinductive + field + node : A ⊎ Delay A + + open Delay + + now : ∀ {A : Set c} → A → Delay A + node (now {A} a) = inj₁ a + + later : ∀ {A : Set c} → Delay A → Delay A + node (later {A} a) = inj₂ a + + never : ∀ {A : Set c} → Delay A + node (never {A}) = inj₂ never + + -- first try + delay-eq-strong : ∀ (A : Setoid c ℓ) → Delay (Setoid.Carrier A) → Delay (Setoid.Carrier A) → Set ℓ + delay-eq-strong A x y with node x | node y + ... | inj₁ a | inj₁ b = Setoid._≈_ A a b + ... | inj₁ a | inj₂ b = ⊥ + ... | inj₂ a | inj₁ b = ⊥ + ... | inj₂ a | inj₂ b = {! !} + + -- second try + record eq-strong (A : Setoid c ℓ) (x : Delay (Setoid.Carrier A)) (y : Delay (Setoid.Carrier A)) : Set c where + field + node-eq₁ : (node x) ≡ (node y) + + -- third try + mutual + node-eq : (A : Setoid c ℓ) (x y : Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → Set ℓ + node-eq A (inj₁ x) (inj₁ y) = Setoid._≈_ A x y + node-eq A (inj₁ x) (inj₂ y) = ⊥ + node-eq A (inj₂ x) (inj₁ y) = ⊥ + node-eq A (inj₂ x) (inj₂ y) = delay-eq-strong' A x y + delay-eq-strong' : ∀ (A : Setoid c ℓ) → Delay (Setoid.Carrier A) → Delay (Setoid.Carrier A) → Set ℓ + delay-eq-strong' A x y = node-eq A {! !} {! !} + + Delay-setoid : Setoid c ℓ → Setoid c ℓ + Delay-setoid A = record { Carrier = Delay A.Carrier ; _≈_ = {! !} ; isEquivalence = {! !} } + where + module A = Setoid A + + + -- finally this should work + mutual + record eq-strong' (A : Setoid c ℓ) (x : Delay (Setoid.Carrier A)) (y : Delay (Setoid.Carrier A)) : Set ℓ where + coinductive + field + eq : eq-strong'' A (node x) (node y) + eq-strong'' : (A : Setoid c ℓ) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → Set ℓ + eq-strong'' A (inj₁ x) (inj₁ y) = Setoid._≈_ A x y + eq-strong'' A (inj₁ x) (inj₂ y) = ⊥ + eq-strong'' A (inj₂ x) (inj₁ y) = ⊥ + eq-strong'' A (inj₂ x) (inj₂ y) = eq-strong' A x y + + + -- this should also work + mutual + record eq-weak (A : Setoid c ℓ) (x : Delay (Setoid.Carrier A)) (y : Delay (Setoid.Carrier A)) : Set ℓ where + coinductive + field + eq : eq-weak' A (node x) (node y) + eq-weak' : (A : Setoid c ℓ) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → (Setoid.Carrier A ⊎ Delay (Setoid.Carrier A)) → Set ℓ + eq-weak' A (inj₁ x) (inj₁ y) = Setoid._≈_ A x y + eq-weak' A (inj₁ x) (inj₂ y) = eq-weak A (now x) y + eq-weak' A (inj₂ x) (inj₁ y) = eq-weak A x (now y) + eq-weak' A (inj₂ x) (inj₂ y) = eq-weak A x y + open eq-weak + + now-cong : ∀ {A : Setoid c ℓ} {a b : Setoid.Carrier A} → Setoid._≈_ A a b → eq-weak A (now a) (now b) + eq (now-cong {A} {a} {b} a≈b) = a≈b + + now-inj : ∀ {A : Setoid c ℓ} {a b : Setoid.Carrier A} → eq-weak A (now a) (now b) → Setoid._≈_ A a b + now-inj {A} {a} {b} na≈nb with (eq na≈nb) + ... | a≈b = a≈b + + now-weak-eq : ∀ {A : Setoid c ℓ} {a : Setoid.Carrier A} {b : Delay (Setoid.Carrier A)} → eq-weak A (now a) b → Σ (Setoid.Carrier A) (λ c → Setoid._≈_ A a c) + now-weak-eq {A} {a} {b} na≈b with node b | eq na≈b + ... | inj₁ x | a≈b = x , a≈b + ... | inj₂ x | a≈b = {! !} + + weak-setoid : Setoid c ℓ → Setoid c ℓ + weak-setoid A = record { Carrier = Delay (Setoid.Carrier A) ; _≈_ = eq-weak A ; isEquivalence = record { refl = refl' ; sym = sym' ; trans = trans' } } + where + refl' : Reflexive (eq-weak A) + eq (refl' {a}) with node a + ... | inj₁ x = IsEquivalence.refl (Setoid.isEquivalence A) + ... | inj₂ x = refl' + sym' : Symmetric (eq-weak A) + eq (sym' {a} {b} a≈b) with node a | node b | eq a≈b + ... | inj₁ x | inj₁ y | z = IsEquivalence.sym (Setoid.isEquivalence A) z + ... | inj₂ x | inj₁ y | z = sym' z + ... | inj₁ x | inj₂ y | z = sym' z + ... | inj₂ x | inj₂ y | z = sym' z + trans' : Transitive (eq-weak A) + eq (trans' {a} {b} {c} a≈b b≈c) with node a | node b | node c | eq a≈b | eq b≈c + ... | inj₂ x | inj₂ y | inj₂ z | eq₁ | eq₂ = trans' eq₁ eq₂ + ... | inj₁ x | inj₂ y | inj₂ z | eq₁ | eq₂ = trans' eq₁ eq₂ + ... | inj₂ x | inj₁ y | inj₂ z | eq₁ | eq₂ = trans' eq₁ eq₂ + ... | inj₁ x | inj₁ y | inj₂ z | eq₁ | eq₂ = trans' (now-cong eq₁) eq₂ -- trans' (now-cong eq₁) eq₂ + ... | inj₂ x | inj₂ y | inj₁ z | eq₁ | eq₂ = trans' eq₁ eq₂ + ... | inj₁ x | inj₂ y | inj₁ z | eq₁ | eq₂ = {! trans' eq₁ eq₂ !} -- now-inj {A} {x} {z} (trans' eq₁ eq₂) + ... | inj₂ x | inj₁ y | inj₁ z | eq₁ | eq₂ = trans' eq₁ (now-cong eq₂) + ... | inj₁ x | inj₁ y | inj₁ z | eq₁ | eq₂ = IsEquivalence.trans (Setoid.isEquivalence A) eq₁ eq₂ +``` \ No newline at end of file diff --git a/src/Monad/Instance/K/Instance/Maybe.lagda.md b/src/Monad/Instance/K/Instance/Maybe.lagda.md index 32d1627..7b312e8 100644 --- a/src/Monad/Instance/K/Instance/Maybe.lagda.md +++ b/src/Monad/Instance/K/Instance/Maybe.lagda.md @@ -147,6 +147,4 @@ Assuming the axiom of choice, the maybe monad is an instance of K in the categor ; identityˡ = λ {A} {i} {j} → identityˡ {A} {i} {j} ; identityʳ = λ {A} {i} {j} → identityʳ {A} {i} {j} } - - ``` \ No newline at end of file