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

minor refactor

Browse source
This commit is contained in:
Leon Vatthauer 2023-12-19 16:01:18 +01:00
parent b5fa52885c
commit 59b105823f
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 127 additions and 115 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -17,7 +17,7 @@ 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 Data.Empty.Polymorphic using (⊥)
open import Categories.NaturalTransformation using (ntHelper)
open import Function.Base using (id)
import Relation.Binary.PropositionalEquality as Eq
@ -37,23 +37,24 @@ 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
open Setoid using () renaming (Carrier to ∣_∣)
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)
data _↓_ : Delay C → C → Set (c ⊔ ℓ) where
data _↓_ : C ⊥ → C → Set (c ⊔ ℓ) where
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↓ : ∀ {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
data _≈_ : Delay C → Delay C → Set (c ⊔ ℓ) where
data _≈_ : C ⊥ → C ⊥ → Set (c ⊔ ℓ) where
↓≈ : ∀ {x y a b} (a∼b : a ∼ b) (x↓a : x ↓ a) (y↓b : y ↓ b) → x ≈ y
later≈ : ∀ {x y} (x≈y : ∞ (♭ x ≈ ♭ y)) → later x ≈ later y
@ -65,11 +66,11 @@ 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))
∼↓ : ∀ {x y : C} {z : Delay C} → x ∼ y → z ↓ x → z ↓ 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 : Delay C} {z : C} → x ≈ y → x ↓ z → y ↓ z
≈↓ : ∀ {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
@ -82,76 +83,74 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
≈-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 } }
-- _⊥ₛ
_⊥ₛ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
_⊥ₛ A = record { Carrier = ∣ A ∣ ⊥ ; _≈_ = _≈_ ; 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 : Setoid c (c ⊔ ℓ)) → (x y : ∣ A ∣ ⊥) → Set (c ⊔ ℓ)
A [ x ≈ y ] = Equality._≈_ {A} x y
_[_∼_] : ∀ (A : Setoid c (c ⊔ ℓ)) → (x y : Setoid.Carrier A) → Set (c ⊔ ℓ)
_[_∼_] : ∀ (A : Setoid c (c ⊔ ℓ)) → (x y : ∣ A ∣) → Set (c ⊔ ℓ)
A [ x ∼ y ] = Setoid._≈_ A x y
∼-refl : ∀ (A : Setoid c (c ⊔ ℓ)) {x : Setoid.Carrier A} → A [ x ∼ x ]
∼-refl : ∀ (A : Setoid c (c ⊔ ℓ)) {x : ∣ 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 : 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 : Setoid.Carrier A} → A [ x ∼ y ] → A [ y ∼ z ] → A [ x ∼ z ]
∼-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 : Setoid.Carrier A} → A [ x ∼ y ] → A [ now x ≈ now 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))
-- slightly different types than later≈
-- TODO remove this is useless
later-cong : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Delay (Setoid.Carrier A)} → A [ x ≈ y ] → A [ later (♯ x) ≈ later (♯ y) ]
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 : Setoid.Carrier A} → A [ now x ≈ now y ] → 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))
liftF : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delay (Setoid.Carrier A) → Delay (Setoid.Carrier B)
liftF : ∀ {A B : Setoid c (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 → delaySetoid A ⟶ delaySetoid B
delayFun : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → A ⊥ₛ ⟶ B ⊥ₛ
delayFun {A} {B} f = record { _⟨$⟩_ = liftF f ; cong = cong' }
where
↓-cong : ∀ {x : Delay (Setoid.Carrier A)} {b : Setoid.Carrier A} → _↓_ {A} x b → _↓_ {B} (liftF f x) (f ⟨$⟩ b)
↓-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 : Delay (Setoid.Carrier A)} → A [ x ≈ y ] → B [ liftF f x ≈ liftF f y ]
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))
-- ↓-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 : 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-self : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Setoid.Carrier A)} → A [ x ≈ later (♯ x) ]
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))
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 : 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)
delayFun-id : ∀ {A : Setoid c (c ⊔ ℓ)} → (delayFun idₛ) ≋ (idₛ {A = delaySetoid A})
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)
@ -172,30 +171,30 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
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))
η : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ delaySetoid A
η : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ A ⊥ₛ
η A = record { _⟨$⟩_ = now ; cong = id λ x∼y → now-cong x∼y }
η↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x y : Setoid.Carrier A} → A [ x ∼ y ] → _↓_ {A} ((η A) ⟨$⟩ 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} 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 : Setoid c (c ⊔ ℓ)} → ∣ (A ⊥ₛ) ⊥ₛ ∣ → ∣ (A ⊥ₛ) ∣
μ' {A} (now x) = x
μ' {A} (later x) = later (♯ μ' {A} (♭ x))
μ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Setoid.Carrier A))} {y : Delay (Setoid.Carrier A)} → _↓_ {delaySetoid A} x y → A [ (μ' {A} x) ≈ y ]
μ↓ : ∀ {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)
-- TODO do delayFun and η in the same style as μ
μ : ∀ (A : Setoid c (c ⊔ ℓ)) → delaySetoid (delaySetoid A) ⟶ delaySetoid A
μ : ∀ (A : Setoid c (c ⊔ ℓ)) → (A ⊥ₛ) ⊥ₛ ⟶ A ⊥ₛ
μ A = record { _⟨$⟩_ = μ' {A} ; cong = cong' }
where
cong' : ∀ {x y : Delay (Delay (Setoid.Carrier A))} → (delaySetoid A) [ x ≈ y ] → A [ μ' {A} x ≈ μ' {A} y ]
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))
@ -208,23 +207,23 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
μ-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 : Delay (Delay (Setoid.Carrier A))} {y : Delay (Setoid.Carrier A)} → _↓_ {delaySetoid 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))))
-- TODO needs another μ↓-trans for when multiple μ's are concerned, i.e. a chain with 3 conditions...
μ↓-trans : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Setoid.Carrier A))} {y : Delay (Setoid.Carrier A)} {z : Setoid.Carrier A} → _↓_ {delaySetoid A} x y → _↓_ {A} y z → _↓_ {A} (μ A ⟨$⟩ x) 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 = ≈↓ (≈-sym 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 (Delay (Setoid.Carrier A)))} {y : Delay (Delay (Setoid.Carrier A))} {z : Delay (Setoid.Carrier A)} → _↓_ {delaySetoid (delaySetoid A)} x y → _↓_ {delaySetoid A} y z → _↓_ {delaySetoid 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 ⊔ ℓ)} → (μ A ∘ (delayFun (μ A))) ≋ (μ A ∘ μ (delaySetoid A))
μ-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))
@ -232,7 +231,7 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
μ-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 : Delay (Setoid.Carrier A)} {y : Setoid.Carrier A} → _↓_ {A} x y → _↓_ {A} ((μ A) ⟨$⟩ ((delayFun (η A)) ⟨$⟩ x)) y
identityˡ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : ∣ A ∣ ⊥} {y : ∣ A ∣} → _↓_ {A} x y → _↓_ {A} ((μ A) ⟨$⟩ ((delayFun (η A)) ⟨$⟩ x)) y
identityˡ↓ {A} {now x} {y} x↓y = x↓y
identityˡ↓ {A} {later x} {y} (later↓ x↓y) = later↓ (identityˡ↓ x↓y)
@ -242,14 +241,14 @@ module Monad.Instance.K.Instance.Delay {c ℓ} where
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 ∘ η (delaySetoid 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
delayMonad : Monad (Setoids c (c ⊔ ℓ))
delayMonad = record
{ F = record
{ F₀ = delaySetoid
{ F₀ = _⊥ₛ
; F₁ = delayFun
; identity = delayFun-id
; homomorphism = delayFun-comp

151
agda/src/Monad/Instance/Setoids/Delay/PreElgot.lagda.md → agda/src/Monad/Instance/Setoids/K.lagda.md
View file

@ -12,67 +12,75 @@ open import Function using (_∘′_) renaming (_∘_ to _∘f_)
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_) renaming (sym to ≡-sym)
open import FreeObject
open import Categories.FreeObjects.Free
open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
open import Categories.Category.Instance.Properties.Setoids.Choice using ()
```
-->
# The delay monad on the category of setoids is pre-Elgot
# The delay monad on the category of setoids is an instance of K
```agda
module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
module Monad.Instance.Setoids.K {ℓ : Level} where
open import Monad.Instance.K.Instance.Delay {ℓ} {ℓ}
open import Category.Ambient.Setoids
open import Monad.Instance.K (setoidAmbient {ℓ})
open import Algebra.Elgot (setoidAmbient {ℓ})
open import Algebra.Elgot.Free (setoidAmbient {ℓ})
open import Category.Construction.ElgotAlgebras (setoidAmbient {ℓ})
open import Monad.PreElgot (setoidAmbient {ℓ})
open Equality
open Setoid using () renaming (Carrier to ∣_∣)
conflict : ∀ {ℓ''} (X Y : Setoid ℓ ℓ) {Z : Set ℓ''}
{x : Setoid.Carrier X} {y : Setoid.Carrier Y } → (X ⊎ₛ Y) [ inj₁ x ∼ inj₂ y ] → Z
{x : ∣ X ∣} {y : ∣ Y ∣} → (X ⊎ₛ Y) [ inj₁ x ∼ inj₂ y ] → Z
conflict X Y ()
iter : ∀ {A X : Setoid ℓ ℓ} → (Setoid.Carrier X → (Delay (Setoid.Carrier A) ⊎ Setoid.Carrier X)) → Setoid.Carrier X → Delay (Setoid.Carrier A)
iter : ∀ {A X : Setoid ℓ ℓ} → (∣ X ∣ → (∣ A ∣ ⊥ ⊎ ∣ X ∣)) → ∣ X ∣ → ∣ A ∣ ⊥
iter {A} {X} f x with f x
... | inj₁ a = a
... | inj₂ b = later (♯ (iter {A} {X} f b))
inj₁-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : Setoid.Carrier X} {a b : Setoid.Carrier Y} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₁ a → f ⟨$⟩ y ≡ inj₁ b → Y [ a ∼ b ]
inj₁-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : ∣ X ∣} {a b : ∣ Y ∣} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₁ a → f ⟨$⟩ y ≡ inj₁ b → Y [ a ∼ b ]
inj₁-helper {X} {Y} f {x} {y} {a} {b} x∼y fi₁ fi₂ = drop-inj₁ {x = a} {y = b} helper
where
helper : (Y ⊎ₛ X) [ inj₁ a ∼ inj₁ b ]
helper rewrite (≡-sym fi₁) | (≡-sym fi₂) = cong f x∼y
inj₂-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : Setoid.Carrier X} {a b : Setoid.Carrier X} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₂ a → f ⟨$⟩ y ≡ inj₂ b → X [ a ∼ b ]
inj₂-helper : ∀ {X Y : Setoid ℓ ℓ} (f : X ⟶ Y ⊎ₛ X) {x y : ∣ X ∣} {a b : ∣ X ∣} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₂ a → f ⟨$⟩ y ≡ inj₂ b → X [ a ∼ b ]
inj₂-helper {X} {Y} f {x} {y} {a} {b} x∼y fi₁ fi₂ = drop-inj₂ {x = a} {y = b} helper
where
helper : (Y ⊎ₛ X) [ inj₂ a ∼ inj₂ b ]
helper rewrite (≡-sym fi₁) | (≡-sym fi₂) = cong f x∼y
absurd-helper : ∀ {ℓ'} {X Y : Setoid ℓ ℓ} {A : Set ℓ'} (f : X ⟶ Y ⊎ₛ X) {x y : Setoid.Carrier X} {a : Setoid.Carrier Y} {b : Setoid.Carrier X} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₁ a → f ⟨$⟩ y ≡ inj₂ b → A
absurd-helper : ∀ {ℓ'} {X Y : Setoid ℓ ℓ} {A : Set ℓ'} (f : X ⟶ Y ⊎ₛ X) {x y : ∣ X ∣} {a : ∣ Y ∣} {b : ∣ X ∣} → X [ x ∼ y ] → f ⟨$⟩ x ≡ inj₁ a → f ⟨$⟩ y ≡ inj₂ b → A
absurd-helper {ℓ'} {X} {Y} {A} f {x} {y} {a} {b} x∼y fi₁ fi₂ = conflict Y X helper
where
helper : (Y ⊎ₛ X) [ inj₁ a ∼ inj₂ b ]
helper rewrite (≡-sym fi₁) | (≡-sym fi₂) = cong f x∼y
iter-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (delaySetoid A ⊎ₛ X)) {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (f ._⟨$⟩_) y ]
iter-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (A ⊥ₛ ⊎ₛ X)) {x y : ∣ X ∣} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (f ._⟨$⟩_) y ]
iter-cong {A} {X} f {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy
... | inj₁ a | inj₁ b = inj₁-helper f x∼y eqx eqy
... | inj₁ a | inj₂ b = absurd-helper f x∼y eqx eqy
... | inj₂ a | inj₁ b = absurd-helper f (∼-sym X x∼y) eqy eqx
... | inj₂ a | inj₂ b = later≈ (♯ iter-cong {A} {X} f (inj₂-helper f x∼y eqx eqy))
iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ [ Function.id , iter {A} {X} (f ._⟨$⟩_) ] ((f ._⟨$⟩_) y) ]
iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (A ⊥ₛ ⊎ₛ X)} {x y : ∣ X ∣} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ [ Function.id , iter {A} {X} (f ._⟨$⟩_) ] ((f ._⟨$⟩_) y) ]
iter-fixpoint {A} {X} {f} {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy
... | inj₁ a | inj₁ b = inj₁-helper f x∼y eqx eqy
... | inj₁ a | inj₂ b = absurd-helper f x∼y eqx eqy
... | inj₂ a | inj₁ b = absurd-helper f (∼-sym X x∼y) eqy eqx
... | inj₂ a | inj₂ b = ≈-sym (later-eq (later≈ (♯ iter-cong f (∼-sym X (inj₂-helper f x∼y eqx eqy)))))
-- iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {g : Y ⟶ (delaySetoid A ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ y) ]
iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (A ⊥ₛ ⊎ₛ X)) → X ⟶ A ⊥ₛ
iterₛ {A} {X} f = record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = iter-cong {A} {X} f }
-- iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (A ⊥ₛ ⊎ₛ X)} {g : Y ⟶ (A ⊥ₛ ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : ∣ X ∣} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ y) ]
-- iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y = ≈-trans (helper x) (iter-cong g (cong h x∼y))
-- where
-- helper : ∀ (x : Setoid.Carrier X) → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ x) ]
-- helper : ∀ (x : ∣ X ∣) → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ x) ]
-- helper x with f ⟨$⟩ x in eqa | g ⟨$⟩ (h ⟨$⟩ x) in eqb
-- ... | inj₁ a | inj₁ b = {! !}
-- ... | inj₁ a | inj₂ b = {! !} -- absurd
@ -80,79 +88,79 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
-- ... | inj₂ a | inj₂ b rewrite (≡-sym eqb) = {! !} -- later≈ (♯ {! iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {a} {(h ⟨$⟩ a)} !}) -- ≈-trans {_} {{! !}} (later≈ {{! !}} {{! !}} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ helper a)) (later≈ (♯ {! !}))
{-# TERMINATING #-}
iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {g : Y ⟶ (delaySetoid A ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ y) ]
iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (A ⊥ₛ ⊎ₛ X)} {g : Y ⟶ (A ⊥ₛ ⊎ₛ Y)} {h : X ⟶ Y} → ([ inj₁ₛ ∘ idₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ∀ {x y : ∣ X ∣} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ y) ]
iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (f ._⟨$⟩_) y in eqy
... | inj₁ a | inj₁ b with g ⟨$⟩ (h ⟨$⟩ y) in eqc
... | inj₁ c = drop-inj₁ {x = a} {y = c} helper
where
helper'' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ [ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ]
helper'' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ [ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ]
helper'' rewrite eqx = ⊎-refl ≈-refl (∼-refl Y)
helper' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ (g ⟨$⟩ (h ⟨$⟩ y)) ]
helper' = ∼-trans ((delaySetoid A) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x∼y)
helper : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ inj₁ c ]
helper' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ (g ⟨$⟩ (h ⟨$⟩ y)) ]
helper' = ∼-trans ((A ⊥ₛ) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x∼y)
helper : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ inj₁ c ]
helper rewrite (≡-sym eqc) = helper'
... | inj₂ c = conflict (delaySetoid A) Y helper
... | inj₂ c = conflict (A ⊥ₛ) Y helper
where
helper'' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ [ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ]
helper'' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ [ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x) ]
helper'' rewrite eqx = ⊎-refl ≈-refl (∼-refl Y)
helper' : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ (g ⟨$⟩ (h ⟨$⟩ y)) ]
helper' = ∼-trans ((delaySetoid A) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x∼y)
helper : (delaySetoid A ⊎ₛ Y) [ inj₁ a ∼ inj₂ c ]
helper' : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ (g ⟨$⟩ (h ⟨$⟩ y)) ]
helper' = ∼-trans ((A ⊥ₛ) ⊎ₛ Y) helper'' (hf≈gh {x} {y} x∼y)
helper : (A ⊥ₛ ⊎ₛ Y) [ inj₁ a ∼ inj₂ c ]
helper rewrite (≡-sym eqc) = helper'
iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₁ a | inj₂ b = absurd-helper f x∼y eqx eqy
iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₂ a | inj₁ b = absurd-helper f (∼-sym X x∼y) eqy eqx
iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh {x} {y} x∼y | inj₂ a | inj₂ b with g ⟨$⟩ (h ⟨$⟩ y) in eqc
... | inj₁ c = conflict (delaySetoid A) Y (∼-sym (delaySetoid A ⊎ₛ Y) helper)
... | inj₁ c = conflict (A ⊥ₛ) Y (∼-sym (A ⊥ₛ ⊎ₛ Y) helper)
where
helper' : (delaySetoid A ⊎ₛ Y) [ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ∼ g ⟨$⟩ (h ⟨$⟩ y) ]
helper' : (A ⊥ₛ ⊎ₛ Y) [ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ∼ g ⟨$⟩ (h ⟨$⟩ y) ]
helper' = hf≈gh {x} {y} x∼y
helper'' : (delaySetoid A ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ]
helper'' rewrite eqx = ∼-refl (delaySetoid A ⊎ₛ Y)
helper : (delaySetoid A ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ inj₁ c ]
helper rewrite (≡-sym eqc) = ∼-trans (delaySetoid A ⊎ₛ Y) helper'' helper'
helper'' : (A ⊥ₛ ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ ([ inj₁ , (λ x₁ → inj₂ (h ⟨$⟩ x₁)) ] (f ⟨$⟩ x)) ]
helper'' rewrite eqx = ∼-refl (A ⊥ₛ ⊎ₛ Y)
helper : (A ⊥ₛ ⊎ₛ Y) [ inj₂ (h ⟨$⟩ a) ∼ inj₁ c ]
helper rewrite (≡-sym eqc) = ∼-trans (A ⊥ₛ ⊎ₛ Y) helper'' helper'
... | inj₂ c = ≈-trans (later≈ {A} {_} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ (iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh (∼-refl X)))) (later≈ (♯ iter-cong g (∼-sym Y helper)))
-- why does this not terminate??
-- | inj₂ c = ≈-trans (later≈ {A} {_} {♯ (iter {A} {Y} (g ._⟨$⟩_)) (h ⟨$⟩ a)} (♯ (iter-uni {A} {X} {Y} {f} {g} {h} hf≈gh (∼-refl X)))) (later≈ (♯ iter-cong g (∼-sym Y helper)))
where
helper''' : (delaySetoid A ⊎ₛ Y) [ inj₂ c ∼ g ⟨$⟩ (h ⟨$⟩ y) ]
helper''' rewrite eqc = ∼-refl (delaySetoid A ⊎ₛ Y)
helper'' : (delaySetoid A ⊎ₛ Y) [ g ⟨$⟩ (h ⟨$⟩ y) ∼ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ]
helper'' = ∼-sym (delaySetoid A ⊎ₛ Y) (hf≈gh x∼y)
helper' : (delaySetoid A ⊎ₛ Y) [ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ∼ inj₂ (h ⟨$⟩ a) ]
helper' rewrite eqx = ∼-refl (delaySetoid A ⊎ₛ Y)
helper''' : (A ⊥ₛ ⊎ₛ Y) [ inj₂ c ∼ g ⟨$⟩ (h ⟨$⟩ y) ]
helper''' rewrite eqc = ∼-refl (A ⊥ₛ ⊎ₛ Y)
helper'' : (A ⊥ₛ ⊎ₛ Y) [ g ⟨$⟩ (h ⟨$⟩ y) ∼ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ]
helper'' = ∼-sym (A ⊥ₛ ⊎ₛ Y) (hf≈gh x∼y)
helper' : (A ⊥ₛ ⊎ₛ Y) [ ([ inj₁ , (λ x₂ → inj₂ (h ⟨$⟩ x₂)) ] (f ⟨$⟩ x)) ∼ inj₂ (h ⟨$⟩ a) ]
helper' rewrite eqx = ∼-refl (A ⊥ₛ ⊎ₛ Y)
helper : Y [ c ∼ h ⟨$⟩ a ]
helper = drop-inj₂ {x = c} {y = h ⟨$⟩ a} (∼-trans (delaySetoid A ⊎ₛ Y) helper''' (∼-trans (delaySetoid A ⊎ₛ Y) helper'' helper'))
helper = drop-inj₂ {x = c} {y = h ⟨$⟩ a} (∼-trans (A ⊥ₛ ⊎ₛ Y) helper''' (∼-trans (A ⊥ₛ ⊎ₛ Y) helper'' helper'))
-- TODO maybe I can improve inj₁-helper etc. to handle this case as well
iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (delaySetoid A ⊎ₛ X)) → f ≋ g → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (g ._⟨$⟩_) y ]
iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (A ⊥ₛ ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → X [ x ∼ y ] → A [ iter {A} {X} (f ._⟨$⟩_) x ≈ iter {A} {X} (g ._⟨$⟩_) y ]
iter-resp-≈ {A} {X} f g f≋g {x} {y} x∼y with (f ._⟨$⟩_) x in eqx | (g ._⟨$⟩_) y in eqy
... | inj₁ a | inj₁ b = drop-inj₁ helper
where
helper : (delaySetoid A ⊎ₛ X) [ inj₁ a ∼ inj₁ b ]
helper : (A ⊥ₛ ⊎ₛ X) [ inj₁ a ∼ inj₁ b ]
helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y
... | inj₁ a | inj₂ b = conflict (delaySetoid A) X helper
... | inj₁ a | inj₂ b = conflict (A ⊥ₛ) X helper
where
helper : (delaySetoid A ⊎ₛ X) [ inj₁ a ∼ inj₂ b ]
helper : (A ⊥ₛ ⊎ₛ X) [ inj₁ a ∼ inj₂ b ]
helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y
... | inj₂ a | inj₁ b = conflict (delaySetoid A) X (∼-sym (delaySetoid A ⊎ₛ X) helper)
... | inj₂ a | inj₁ b = conflict (A ⊥ₛ) X (∼-sym (A ⊥ₛ ⊎ₛ X) helper)
where
helper : (delaySetoid A ⊎ₛ X) [ inj₂ a ∼ inj₁ b ]
helper : (A ⊥ₛ ⊎ₛ X) [ inj₂ a ∼ inj₁ b ]
helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y
... | inj₂ a | inj₂ b = later≈ (♯ iter-resp-≈ {A} {X} f g f≋g (drop-inj₂ helper))
where
helper : (delaySetoid A ⊎ₛ X) [ inj₂ a ∼ inj₂ b ]
helper : (A ⊥ₛ ⊎ₛ X) [ inj₂ a ∼ inj₂ b ]
helper rewrite (≡-sym eqy) | (≡-sym eqx) = f≋g x∼y
iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (delaySetoid A ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : Setoid.Carrier (X ⊎ₛ Y)} → (X ⊎ₛ Y) [ x ∼ y ] → A [ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} (f ._⟨$⟩_) , inj₂ ∘f (h ._⟨$⟩_) ] x ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f (f ._⟨$⟩_) , (inj₂ ∘f (h ._⟨$⟩_)) ] y ]
iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (A ⊥ₛ ⊎ₛ X)} {h : Y ⟶ X ⊎ₛ Y} {x y : ∣ X ⊎ₛ Y ∣} → (X ⊎ₛ Y) [ x ∼ y ] → A [ iter {A} {X ⊎ₛ Y} [ inj₁ ∘f iter {A} {X} (f ._⟨$⟩_) , inj₂ ∘f (h ._⟨$⟩_) ] x ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘f (f ._⟨$⟩_) , (inj₂ ∘f (h ._⟨$⟩_)) ] y ]
iter-folding {A} {X} {Y} {f} {h} {inj₁ x} {inj₁ y} ix∼iy with f ⟨$⟩ x in eqx | f ⟨$⟩ y in eqy
... | inj₁ a | inj₁ b = inj₁-helper f (drop-inj₁ ix∼iy) eqx eqy
... | inj₁ a | inj₂ b = absurd-helper f (drop-inj₁ ix∼iy) eqx eqy
... | inj₂ a | inj₁ b = absurd-helper f (∼-sym X (drop-inj₁ ix∼iy)) eqy eqx
... | inj₂ a | inj₂ b = later≈ (♯ ≈-trans (iter-cong f (inj₂-helper f (drop-inj₁ ix∼iy) eqx eqy)) (helper b))
where
helper : ∀ (b : Setoid.Carrier X) → A [ iter {A} {X} (f ._⟨$⟩_) b ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ (f ._⟨$⟩_) , inj₂ ∘′ (h ._⟨$⟩_) ] (inj₁ b) ]
helper : ∀ (b : ∣ X ∣) → A [ iter {A} {X} (f ._⟨$⟩_) b ≈ iter {A} {X ⊎ₛ Y} [ [ inj₁ , inj₂ ∘′ inj₁ ] ∘′ (f ._⟨$⟩_) , inj₂ ∘′ (h ._⟨$⟩_) ] (inj₁ b) ]
helper b with f ⟨$⟩ b in eqb
... | inj₁ c = ∼-refl (delaySetoid A)
... | inj₁ c = ∼-refl (A ⊥ₛ)
... | inj₂ c = later≈ (♯ helper c)
iter-folding {A} {X} {Y} {f} {h} {inj₂ x} {inj₂ y} ix∼iy with h ⟨$⟩ x in eqx | h ⟨$⟩ y in eqy
... | inj₁ a | inj₁ b = later≈ (♯ iter-folding {A} {X} {Y} {f} {h} {inj₁ a} {inj₁ b} helper)
@ -166,9 +174,9 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
helper : (X ⊎ₛ Y) [ inj₂ a ∼ inj₂ b ]
helper rewrite (≡-sym eqx) | (≡-sym eqy) = cong h (drop-inj₂ ix∼iy)
delay-algebras-on : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (delaySetoid A)
delay-algebras-on : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (A ⊥ₛ)
delay-algebras-on {A} = record
{ _# = λ {X} f → record { _⟨$⟩_ = iter {A} {X} (f ._⟨$⟩_) ; cong = λ {x} {y} x∼y → iter-cong {A} {X} f {x} {y} x∼y }
{ _# = iterₛ {A}
; #-Fixpoint = λ {X} {f} → iter-fixpoint {A} {X} {f}
; #-Uniformity = λ {X} {Y} {f} {g} {h} → iter-uni {A} {X} {Y} {f} {g} {h}
; #-Folding = λ {X} {Y} {f} {h} {x} {y} x∼y → iter-folding {A} {X} {Y} {f} {h} {x} {y} x∼y
@ -176,32 +184,37 @@ module Monad.Instance.Setoids.Delay.PreElgot {ℓ : Level} where
}
delay-algebras : ∀ (A : Setoid ℓ ℓ) → Elgot-Algebra
delay-algebras A = record { A = delaySetoid A ; algebra = delay-algebras-on {A} }
delay-algebras A = record { A = A ⊥ₛ ; algebra = delay-algebras-on {A}}
isFreeAlgebra : ∀ {A : Setoid ℓ ℓ} → IsFreeObject elgotForgetfulF (delaySetoid A) (delay-algebras A)
isFreeAlgebra {A} = record
{ η = SΠ.id
; _* = λ {B} f → record { h = f ; preserves = λ {X} {g} {x} {y} x∼y → *-preserves {B} f {X} {g} {x} {y} x∼y }
; *-lift = λ {B} f {x} {y} x∼y → cong f x∼y
; *-uniq = λ {B} f g g≋f {x} {y} x∼y → g≋f x∼y
}
where
-- TODO use fixpoint for this
*-preserves : ∀ {B : Elgot-Algebra} (f : delaySetoid A ⟶ Elgot-Algebra.A B) {X : Setoid ℓ ℓ} {g : X ⟶ (delaySetoid A) ⊎ₛ X} → ∀ {x y : Setoid.Carrier X} → X [ x ∼ y ] → Elgot-Algebra.A B [ (f ._⟨$⟩_ ∘′ iter {A} {X} (g ._⟨$⟩_)) x ∼ ((B Elgot-Algebra.#) _) ⟨$⟩ y ]
*-preserves {B} f {X} {g} {x} {y} x∼y = ∼-sym (Elgot-Algebra.A B) (∼-trans (Elgot-Algebra.A B) (#-Fixpoint (∼-sym X x∼y)) helper)
where
open Elgot-Algebra B using (#-Fixpoint)
helper : Elgot-Algebra.A B [ {! !} x ∼ (f ._⟨$⟩_ ∘′ iter {A} {X} (g ._⟨$⟩_)) x ] -- ([ (f ._⟨$⟩_) , _ ] ∘′ g ._⟨$⟩_)
helper with g ⟨$⟩ x in eqx
... | inj₁ a = {! !}
... | inj₂ b = {! !}
open Elgot-Algebra using () renaming (A to ⟦_⟧)
-- TODO remove
delayPreElgot : IsPreElgot delayMonad
delayPreElgot = record
{ elgotalgebras = delay-algebras-on
; extend-preserves = {! !}
nowₛ : ∀ {A : Setoid ℓ ℓ} → A ⟶ A ⊥ₛ
nowₛ = record { _⟨$⟩_ = now ; cong = now-cong }
delay-lift' : ∀ {A B : Set ℓ} → (A → B) → A ⊥ → B
delay-lift' {A} {B} f (now x) = f x
delay-lift' {A} {B} f (later x) = {! !}
delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
delay-lift {A} {B} f = record { h = record { _⟨$⟩_ = delay-lift' {∣ A ∣} {∣ ⟦ B ⟧ ∣} (f ._⟨$⟩_) ; cong = {! !} } ; preserves = {! !} }
freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A
freeAlgebra A = record
{ FX = delay-algebras A
; η = nowₛ {A}
; _* = delay-lift
; *-lift = {! !}
; *-uniq = {! !}
}
isStableFreeElgotAlgebra : ∀ (A : Setoid ℓ ℓ) → IsStableFreeElgotAlgebra (freeAlgebra A)
isStableFreeElgotAlgebra A = record
{ [_,_]♯ = {! !}
; ♯-law = {! !}
; ♯-preserving = {! !}
; ♯-unique = {! !}
}
delayK : MonadK
delayK = record { freealgebras = freeAlgebra ; stable = isStableFreeElgotAlgebra }
```