leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

Work on delay example

Browse source
This commit is contained in:
Leon Vatthauer 2023-12-05 20:52:53 +01:00
parent be0971ae42
commit 64c4a4263d
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
3 changed files with 321 additions and 126 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

263
agda/src/Monad/Instance/K/Instance/Delay.lagda.md
View file

@ -4,7 +4,7 @@
open import Level
open import Category.Ambient using (Ambient)
open import Categories.Category
open import Categories.Category.Core
open import Categories.Category.Instance.Setoids
open import Categories.Monad
open import Categories.Category.Monoidal.Instance.Setoids
@ -23,6 +23,8 @@ 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
import Category.Monad.Partiality
```
-->
@ -33,125 +35,164 @@ 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
data Delay (A : Set c) : Set c where
now : A → Delay A
later : ∞ (Delay A) → Delay A
now : ∀ {A : Set c} → A → Delay A
node (now {A} a) = inj₁ 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)
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
module Equality {A : Setoid c ℓ} where
open Setoid A using () renaming (Carrier to C; _≈_ to _∼_)
data _↓_ : Delay C → C → Set (c ⊔ ℓ) where
now↓ : ∀ {x y} (p : x ∼ y) → now x ↓ y
later↓ : ∀ {x y} (p : _↓_ x y) → later x ↓ y
now↓ : ∀ {x y} (x∼y : x ∼ y) → now x ↓ y
later↓ : ∀ {x y} (x↓y : ♭ x ↓ y) → later x ↓ y
unique↓ : ∀ {c : Delay 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
data _≈_ : Delay C → Delay C → Set (c ⊔ ℓ) where
↓≈ : ∀ {x y z} → x ↓ z → y ↓ z → x ≈ y
later-≈ : ∀ {x y} → x ≈ y → later x ≈ later y
↓≈ : ∀ {x y a b} (a∼b : a ∼ b) (x↓a : x ↓ a) (y↓b : y ↓ b) → x ≈ y
later≈ : ∀ {x y} → (∞ (♭ x ≈ ♭ y)) → later x ≈ later y
refl : ∀ {x} → x ≈ x
refl {x} with node x
... | inj₁ z = ↓≈ {! !} {! !}
... | inj₂ z = {! !}
≈-refl : ∀ {x} → x ≈ x
≈-refl {now x} = ↓≈ ∼-refl (now↓ ∼-refl) (now↓ ∼-refl)
≈-refl {later x} = later≈ (♯ ≈-refl)
-- 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 = {! !}
≈-sym : ∀ {x y} → x ≈ y → y ≈ x
≈-sym (↓≈ a∼b x↓a y↓b) = ↓≈ (∼-sym a∼b) y↓b x↓a
≈-sym (later≈ x≈y) = later≈ (♯ ≈-sym (♭ x≈y))
∼↓ : ∀ {x y : C} {z : Delay 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 : Delay 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
≈↓ (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 (later≈ x≈y) (later≈ y≈z) = later≈ (♯ ≈-trans (♭ x≈y) (♭ y≈z))
delaySetoid : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
delaySetoid A = record { Carrier = Delay Carrier ; _≈_ = _≈_ ; isEquivalence = record { refl = ≈-refl ; sym = ≈-sym ; trans = ≈-trans } }
where
open Setoid A using (Carrier)
open Equality {A}
open Equality using (↓≈; later≈; now↓; later↓; _↓_; ≈↓; ≈-refl; ≈-sym; ≈-trans)
_[_≈_] : ∀ (A : Setoid c (c ⊔ ℓ)) → (x y : Delay (Setoid.Carrier A)) → Set (c ⊔ ℓ)
A [ x ≈ y ] = Equality._≈_ {A} x y
_[_∼_] : ∀ (A : Setoid c (c ⊔ ℓ)) → (x y : Setoid.Carrier A) → Set (c ⊔ ℓ)
A [ x ∼ y ] = Setoid._≈_ A x y
∼-refl : ∀ (A : Setoid c (c ⊔ ℓ)) {x : Setoid.Carrier A} → A [ x ∼ x ]
∼-refl A = IsEquivalence.refl (Setoid.isEquivalence A)
∼-sym : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Setoid.Carrier A} → A [ x ∼ y ] → A [ y ∼ x ]
∼-sym A = IsEquivalence.sym (Setoid.isEquivalence A)
∼-trans : ∀ (A : Setoid c (c ⊔ ℓ)) {x y z : Setoid.Carrier 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 : Setoid.Carrier A} → A [ x ∼ y ] → A [ now x ≈ now y ]
now-cong {A} {x} {y} x∼y = ↓≈ x∼y (now↓ (∼-refl A)) (now↓ (∼-refl A))
delayFun : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → delaySetoid A ⟶ delaySetoid B
delayFun {A} {B} f = record { _⟨$⟩_ = app ; cong = cong' }
where
app : Delay (Setoid.Carrier A) → Delay (Setoid.Carrier B)
app (now x) = now (f ⟨$⟩ x)
app (later x) = later (♯ app (♭ x))
-- TODO a variant of this should be useful outside
↓-cong : ∀ {x : Delay (Setoid.Carrier A)} {b : Setoid.Carrier A} → _↓_ {A} x b → _↓_ {B} (app 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 : Delay (Setoid.Carrier A)} → A [ x ≈ y ] → B [ app x ≈ app 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))
-- ↓-delay : ∀ {A B : Setoid c ℓ} (f : A ⟶ B) {x : Setoid.Carrier → f ⟨$⟩ x
-- 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 : Delay (Setoid.Carrier 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-self : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Setoid.Carrier 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))
delayFun↓ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x : Delay (Setoid.Carrier A)} {y : Setoid.Carrier 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)
delayFun-id : ∀ {A : Setoid c (c ⊔ ℓ)} → (delayFun idₛ) ≋ (idₛ {A = delaySetoid 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))
η : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ delaySetoid A
η A = record { _⟨$⟩_ = now ; cong = id λ x∼y → now-cong x∼y }
η-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (η B ∘ f) ≋ (delayFun f ∘ η A)
η-natural {A} {B} f {x} {y} x≈y = now-cong (cong f x≈y)
private
μ' : ∀ {A : Setoid c (c ⊔ ℓ)} → Setoid.Carrier (delaySetoid (delaySetoid A)) → Setoid.Carrier (delaySetoid A)
μ' {A} (now x) = x
μ' {A} (later x) = later (♯ μ' {A} (♭ x))
μ↓ : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) {x : Delay (Delay (Setoid.Carrier A))} {y : Delay (Setoid.Carrier A)} → _↓_ {delaySetoid A} x y → A [ (μ' {A} x) ≈ y ]
μ↓ {A} {B} f {now x} {y} (now↓ x≈y) = x≈y
μ↓ {A} {B} f {later x} {y} (later↓ x↓y) = ≈-trans (later≈ (♯ μ↓ f x↓y)) (≈-sym later-self)
-- TODO μ≈
-- TODO do delayFun and η in the same style as μ
-- 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 = {! !} }
μ : ∀ (A : Setoid c (c ⊔ ℓ)) → delaySetoid (delaySetoid A) ⟶ delaySetoid A
μ A = record { _⟨$⟩_ = μ' {A} ; cong = {! !} }
where
module A = Setoid A
cong' : ∀ {x y : Delay (Delay (Setoid.Carrier A))} → (delaySetoid A) [ x ≈ y ] → A [ μ' x ≈ μ' y ]
cong' {now x} {now y} (↓≈ a≈b (now↓ x≈a) (now↓ y≈b)) = ≈-trans x≈a (≈-trans a≈b (≈-sym y≈b))
cong' {now x} {later y} (↓≈ a≈b (now↓ x≈a) (later↓ y↓b)) = ↓≈ {A} {! a≈b !} {! !} (later↓ {! !})
cong' {later x} {now y} (↓≈ a≈b (later↓ x↓a) (now↓ (↓≈ a∼b x↓a₁ y↓b))) = ↓≈ {! !} (later↓ {! !}) x↓a₁
cong' {later x} {now .(later _)} (↓≈ a≈b (later↓ x↓a) (now↓ (later≈ x₁))) = ↓≈ {! !} {! !} {! !}
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))
delayMonad : Monad (Setoids c (c ⊔ ℓ))
delayMonad = record
{ F = record
{ F₀ = delaySetoid
; F₁ = delayFun
; identity = delayFun-id
; homomorphism = {! !}
; F-resp-≈ = {! !}
}
; η = ntHelper (record { η = η ; commute = η-natural })
; μ = {! !}
; assoc = {! !}
; sym-assoc = {! !}
; identityˡ = {! !}
; identityʳ = {! !}
}
-- 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₂ = {! !} -- 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₂
```

27
agda/src/Monad/Instance/K/Instance/Delay'.lagda.md → agda/src/Monad/Instance/K/Instance/DelayOld.lagda.md
View file

@ -29,7 +29,7 @@ import Category.Monad.Partiality
-->
```agda
module Monad.Instance.K.Instance.Delay' {c ℓ} where
module Monad.Instance.K.Instance.DelayOld {c ℓ} where
```
# Capretta's Delay Monad is an Instance of K in the Category of Setoids
@ -39,11 +39,6 @@ module Monad.Instance.K.Instance.Delay' {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
@ -130,20 +125,22 @@ module Monad.Instance.K.Instance.Delay' {c ℓ} where
sym' (↓≈ a∼b x↓a y↓b) = ↓≈ (∼-sym a∼b) y↓b x↓a
sym' (later≈ x≈y) = later≈ (♯ sym' (♭ x≈y))
-- TODO needed for trans'
∼↓ : ∀ {x y : C} {z : Delay 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 : Delay C} {z : C} → x ≈ y → x ↓ z → y ↓ z
≈↓ x≈y x↓z = {! !}
-- ≈↓ (↓≈ a(now↓ refl) q) (now↓ refl) = q
-- ≈↓ (↓≈ (later↓ p) r) (later↓ q) with unique↓ p q
-- ≈↓ (↓≈ (later↓ p) r) (later↓ q) | refl = r
-- ≈↓ (later≈ p) (later↓ q) = later↓ (≈↓ (♭ p) q)
≈↓ (↓≈ 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
≈↓ (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 x↓a (later↓ y↓b)) (later≈ x) = ↓≈ a∼b x↓a {! !}
trans' (later≈ x) (↓≈ a∼b x↓a y↓b) = {! !}
trans' (later≈ x) (later≈ y) = {! !}
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))
delay-setoid' : Setoid c ℓ → Setoid c (c ⊔ ℓ)
delay-setoid' A = record { Carrier = Delay Carrier ; _≈_ = _≈_ ; isEquivalence = record { refl = λ {x} → {! !} ; sym = λ {x y} → {! !} ; trans = λ {x y z} → {! !} } }

157
agda/src/Monad/Instance/K/Instance/DelayRecord.lagda.md Normal file
View file

@ -0,0 +1,157 @@
<!--
```agda
{-# OPTIONS --allow-unsolved-metas --guardedness #-}
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)
```
-->
```agda
module Monad.Instance.K.Instance.DelayRecord {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
module Equality {A : Setoid c ℓ} where
open Setoid A using () renaming (Carrier to C; _≈_ to _∼_)
data _↓_ : Delay C → C → Set (c ⊔ ℓ) where
now↓ : ∀ {x y} (p : x ∼ y) → now x ↓ y
later↓ : ∀ {x y} (p : _↓_ x y) → later x ↓ y
data _≈_ : Delay C → Delay C → Set (c ⊔ ℓ) where
↓≈ : ∀ {x y z} → x ↓ z → y ↓ z → x ≈ y
later-≈ : ∀ {x y} → x ≈ y → later x ≈ later y
refl : ∀ {x} → x ≈ x
refl {x} with node x
... | inj₁ z = ↓≈ {! !} {! !}
... | inj₂ z = {! !}
-- 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₂ = {! !} -- 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₂
```