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

sync

Browse source
This commit is contained in:
Leon Vatthauer 2024-02-15 16:03:26 +01:00
parent cc0cb9cd18
commit 8caee3929a
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
4 changed files with 155 additions and 106 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

58
agda/src/Monad/Instance/Setoids/Delay.lagda.md
View file

@ -176,10 +176,10 @@ open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼
module DelayMonad where module DelayMonad where
Delayₛ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ) Delay≈ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
Delayₛ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_≈_] A ; isEquivalence = record { refl = ≈-refl A ; sym = ≈-sym A ; trans = ≈-trans A } } Delay≈ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_≈_] A ; isEquivalence = record { refl = ≈-refl A ; sym = ≈-sym A ; trans = ≈-trans A } }
Delayₛ∼ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ) Delay∼ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ)
Delayₛ∼ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_∼_] A ; isEquivalence = record { refl = ∼-refl A ; sym = ∼-sym A ; trans = ∼-trans A } } Delay∼ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_∼_] A ; isEquivalence = record { refl = ∼-refl A ; sym = ∼-sym A ; trans = ∼-trans A } }
<_> = _⟨$⟩_ <_> = _⟨$⟩_
open _⟶_ using (cong) open _⟶_ using (cong)
@ -220,10 +220,10 @@ module DelayMonad where
lift-cong {A} {B} f {later x} {later y} (later≈ x≈y) = later≈ (lift-cong′ {A} {B} f x≈y) lift-cong {A} {B} f {later x} {later y} (later≈ x≈y) = later≈ (lift-cong′ {A} {B} f x≈y)
force≈ (lift-cong′ {A} {B} f {x} {y} x≈y) = lift-cong f (force≈ x≈y) force≈ (lift-cong′ {A} {B} f {x} {y} x≈y) = lift-cong f (force≈ x≈y)
liftFₛ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delayₛ A ⟶ Delayₛ B liftFₛ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delay≈ A ⟶ Delay≈ B
liftFₛ {A} {B} f = record { to = liftF < f > ; cong = lift-cong f } liftFₛ {A} {B} f = record { to = liftF < f > ; cong = lift-cong f }
liftFₛ∼ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delayₛ∼ A ⟶ Delayₛ∼ B liftFₛ∼ : ∀ {A B : Setoid c (c ⊔ ℓ)} → A ⟶ B → Delay∼ A ⟶ Delay∼ B
liftFₛ∼ {A} {B} f = record { to = liftF < f > ; cong = ∼-cong } liftFₛ∼ {A} {B} f = record { to = liftF < f > ; cong = ∼-cong }
where where
∼-cong : ∀ {x y} → [ A ][ x ∼ y ] → [ B ][ liftF < f > x ∼ liftF < f > y ] ∼-cong : ∀ {x y} → [ A ][ x ∼ y ] → [ B ][ liftF < f > x ∼ liftF < f > y ]
@ -258,7 +258,7 @@ module DelayMonad where
later-eq {A} {x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ↓≈ a≡b x↓a (now↓ y≡b) later-eq {A} {x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ↓≈ a≡b x↓a (now↓ y≡b)
later-eq {A} {x} {later y} x≈ly = ≈-trans A later-self x≈ly later-eq {A} {x} {later y} x≈ly = ≈-trans A later-self x≈ly
lift-id : ∀ {A : Setoid c (c ⊔ ℓ)} → (liftFₛ (idₛ A)) ≋ (idₛ (Delayₛ A)) lift-id : ∀ {A : Setoid c (c ⊔ ℓ)} → (liftFₛ (idₛ A)) ≋ (idₛ (Delay≈ A))
lift-id′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay ∣ A ∣} → [ A ][ (liftF id) x ≈′ id x ] lift-id′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay ∣ A ∣} → [ A ][ (liftF id) x ≈′ id x ]
lift-id {A} {now x} = ≈-refl A lift-id {A} {now x} = ≈-refl A
lift-id {A} {later x} = later≈ lift-id′ lift-id {A} {later x} = later≈ lift-id′
@ -276,7 +276,7 @@ module DelayMonad where
lift-resp-≈ {A} {B} {f} {g} f≋g {later x} = later≈ (lift-resp-≈′ {A} {B} {f} {g} f≋g) lift-resp-≈ {A} {B} {f} {g} f≋g {later x} = later≈ (lift-resp-≈′ {A} {B} {f} {g} f≋g)
force≈ (lift-resp-≈′ {A} {B} {f} {g} f≋g {x}) = lift-resp-≈ {A} {B} {f} {g} f≋g force≈ (lift-resp-≈′ {A} {B} {f} {g} f≋g {x}) = lift-resp-≈ {A} {B} {f} {g} f≋g
ηₛ : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ Delayₛ A ηₛ : ∀ (A : Setoid c (c ⊔ ℓ)) → A ⟶ Delay≈ A
ηₛ A = record { to = now ; cong = now-cong } ηₛ A = record { to = now ; cong = now-cong }
η-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (ηₛ B ∘ f) ≋ (liftFₛ f ∘ ηₛ A) η-natural : ∀ {A B : Setoid c (c ⊔ ℓ)} (f : A ⟶ B) → (ηₛ B ∘ f) ≋ (liftFₛ f ∘ ηₛ A)
@ -288,35 +288,35 @@ module DelayMonad where
μ {A} (now x) = x μ {A} (now x) = x
μ {A} (later x) = later (μ′ {A} x) μ {A} (later x) = later (μ′ {A} x)
μ↓-trans : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} {b : ∣ A ∣} → [ Delayₛ A ][ x ↓ y ] → [ A ][ y ↓ b ] → [ A ][ (μ {A} x) ↓ b ] μ↓-trans : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} {b : ∣ A ∣} → [ Delay≈ A ][ x ↓ y ] → [ A ][ y ↓ b ] → [ A ][ (μ {A} x) ↓ b ]
μ↓-trans {A} {now x} {y} {b} (now↓ x≡y) y↓b = ≈↓ A (≈-sym A x≡y) y↓b μ↓-trans {A} {now x} {y} {b} (now↓ x≡y) y↓b = ≈↓ A (≈-sym A x≡y) y↓b
μ↓-trans {A} {later x} {now y} {b} (later↓ x↓y) (now↓ y≡b) = later↓ (μ↓-trans x↓y (now↓ y≡b)) μ↓-trans {A} {later x} {now y} {b} (later↓ x↓y) (now↓ y≡b) = later↓ (μ↓-trans x↓y (now↓ y≡b))
μ↓-trans {A} {later x} {later y} {b} (later↓ x↓y) (later↓ y↓b) = later↓ (μ↓-trans (≡↓ (Delayₛ A) (≈-sym A later-self) x↓y) y↓b) μ↓-trans {A} {later x} {later y} {b} (later↓ x↓y) (later↓ y↓b) = later↓ (μ↓-trans (≡↓ (Delay≈ A) (≈-sym A later-self) x↓y) y↓b)
μ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} → [ Delayₛ A ][ x ↓ y ] → [ A ][ (μ {A} x) ≈ y ] μ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} → [ Delay≈ A ][ x ↓ y ] → [ A ][ (μ {A} x) ≈ y ]
μ↓′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} → [ Delayₛ A ][ x ↓ y ] → [ A ][ (μ {A} x) ≈′ y ] μ↓′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay ∣ A ∣)} {y : Delay ∣ A ∣} → [ Delay≈ A ][ x ↓ y ] → [ A ][ (μ {A} x) ≈′ y ]
force≈ (μ↓′ {A} {x} {y} x↓y) = μ↓ x↓y force≈ (μ↓′ {A} {x} {y} x↓y) = μ↓ x↓y
μ↓ {A} {now x} {y} (now↓ x≡y) = x≡y μ↓ {A} {now x} {y} (now↓ x≡y) = x≡y
μ↓ {A} {later x} {now y} (later↓ x↓y) = ≈-trans A (≈-sym A later-self) (↓≈ (≡-refl A) (μ↓-trans x↓y (now↓ (≡-refl A))) (now↓ (≡-refl A))) μ↓ {A} {later x} {now y} (later↓ x↓y) = ≈-trans A (≈-sym A later-self) (↓≈ (≡-refl A) (μ↓-trans x↓y (now↓ (≡-refl A))) (now↓ (≡-refl A)))
μ↓ {A} {later x} {later y} (later↓ x↓y) = later≈ (μ↓′ {A} {force x} {force y} (≡↓ (Delayₛ A) (≈-sym A later-self) x↓y)) μ↓ {A} {later x} {later y} (later↓ x↓y) = later≈ (μ↓′ {A} {force x} {force y} (≡↓ (Delay≈ A) (≈-sym A later-self) x↓y))
μ-cong : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ A ][ x ≈ y ] → [ A ][ μ {A} x ≈ μ {A} y ] μ-cong : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delay≈ A ][ x ≈ y ] → [ A ][ μ {A} x ≈ μ {A} y ]
μ-cong′ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ A ][ x ≈′ y ] → [ A ][ μ {A} x ≈′ μ {A} y ] μ-cong′ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delay≈ A ][ x ≈′ y ] → [ A ][ μ {A} x ≈′ μ {A} y ]
μ-cong A {now x} {now y} x≈y = now-inj x≈y μ-cong A {now x} {now y} x≈y = now-inj x≈y
μ-cong A {now x} {later y} (↓≈ a≡b (now↓ x≡a) (later↓ y↓b)) = ≈-trans A (≈-sym A (μ↓ (≡↓ (Delayₛ A) (≈-trans A (≈-sym A a≡b) (≈-sym A x≡a)) y↓b))) later-self μ-cong A {now x} {later y} (↓≈ a≡b (now↓ x≡a) (later↓ y↓b)) = ≈-trans A (≈-sym A (μ↓ (≡↓ (Delay≈ A) (≈-trans A (≈-sym A a≡b) (≈-sym A x≡a)) y↓b))) later-self
μ-cong A {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ≈-trans A (≈-sym A later-self) (μ↓ (≡↓ (Delayₛ A) (≈-trans A a≡b (≈-sym A y≡b)) x↓a)) μ-cong A {later x} {now y} (↓≈ a≡b (later↓ x↓a) (now↓ y≡b)) = ≈-trans A (≈-sym A later-self) (μ↓ (≡↓ (Delay≈ A) (≈-trans A a≡b (≈-sym A y≡b)) x↓a))
μ-cong A {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (μ-cong′ A (≈→≈′ (Delayₛ A) (↓≈ a≡b x↓a y↓b))) μ-cong A {later x} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (μ-cong′ A (≈→≈′ (Delay≈ A) (↓≈ a≡b x↓a y↓b)))
μ-cong A {later x} {later y} (later≈ x≈y) = later≈ (μ-cong′ A x≈y) μ-cong A {later x} {later y} (later≈ x≈y) = later≈ (μ-cong′ A x≈y)
force≈ (μ-cong′ A {x} {y} x≈y) = μ-cong A (force≈ x≈y) force≈ (μ-cong′ A {x} {y} x≈y) = μ-cong A (force≈ x≈y)
μₛ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delayₛ (Delayₛ A) ⟶ Delayₛ A μₛ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delay≈ (Delay≈ A) ⟶ Delay≈ A
μₛ A = record { to = μ {A} ; cong = μ-cong A } μₛ A = record { to = μ {A} ; cong = μ-cong A }
μₛ∼ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delayₛ∼ (Delayₛ∼ A) ⟶ Delayₛ∼ A μₛ∼ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delay∼ (Delay∼ A) ⟶ Delay∼ A
μₛ∼ A = record { to = μ {A} ; cong = μ-cong∼ A } μₛ∼ A = record { to = μ {A} ; cong = μ-cong∼ A }
where where
μ-cong∼ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ∼ A ][ x ∼ y ] → [ A ][ μ {A} x ∼ μ {A} y ] μ-cong∼ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delay∼ A ][ x ∼ y ] → [ A ][ μ {A} x ∼ μ {A} y ]
μ-cong∼′ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delayₛ∼ A ][ x ∼′ y ] → [ A ][ μ {A} x ∼′ μ {A} y ] μ-cong∼′ : ∀ (A : Setoid c (c ⊔ ℓ)) {x y : Delay (Delay ∣ A ∣)} → [ Delay∼ A ][ x ∼′ y ] → [ A ][ μ {A} x ∼′ μ {A} y ]
force∼ (μ-cong∼′ A {x} {y} x∼y) = μ-cong∼ A (force∼ x∼y) force∼ (μ-cong∼′ A {x} {y} x∼y) = μ-cong∼ A (force∼ x∼y)
μ-cong∼ A {.(now _)} {.(now _)} (now∼ x∼y) = x∼y μ-cong∼ A {.(now _)} {.(now _)} (now∼ x∼y) = x∼y
μ-cong∼ A {.(later _)} {.(later _)} (later∼ x∼y) = later∼ (μ-cong∼′ A x∼y) μ-cong∼ A {.(later _)} {.(later _)} (later∼ x∼y) = later∼ (μ-cong∼′ A x∼y)
@ -327,13 +327,13 @@ module DelayMonad where
μ-natural {A} {B} f {now x} = ≈-refl B μ-natural {A} {B} f {now x} = ≈-refl B
μ-natural {A} {B} f {later x} = later≈ (μ-natural′ f {force x}) μ-natural {A} {B} f {later x} = later≈ (μ-natural′ f {force x})
μ-assoc' : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Delay ∣ A ∣))} → [ A ][ (μₛ A ∘ (liftFₛ (μₛ A))) ⟨$⟩ x ∼ (μₛ A ∘ μₛ (Delayₛ A)) ⟨$⟩ x ] μ-assoc' : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Delay ∣ A ∣))} → [ A ][ (μₛ A ∘ (liftFₛ (μₛ A))) ⟨$⟩ x ∼ (μₛ A ∘ μₛ (Delay≈ A)) ⟨$⟩ x ]
μ-assoc'′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Delay ∣ A ∣))} → [ A ][ (μₛ A ∘ (liftFₛ (μₛ A))) ⟨$⟩ x ∼′ (μₛ A ∘ μₛ (Delayₛ A)) ⟨$⟩ x ] μ-assoc'′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay (Delay (Delay ∣ A ∣))} → [ A ][ (μₛ A ∘ (liftFₛ (μₛ A))) ⟨$⟩ x ∼′ (μₛ A ∘ μₛ (Delay≈ A)) ⟨$⟩ x ]
force∼ (μ-assoc'′ {A} {x}) = μ-assoc' {A} {x} force∼ (μ-assoc'′ {A} {x}) = μ-assoc' {A} {x}
μ-assoc' {A} {now x} = ∼-refl A μ-assoc' {A} {now x} = ∼-refl A
μ-assoc' {A} {later x} = later∼ (μ-assoc'′ {A} {force x}) μ-assoc' {A} {later x} = later∼ (μ-assoc'′ {A} {force x})
μ-assoc : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ (liftFₛ (μₛ A))) ≋ (μₛ A ∘ μₛ (Delayₛ A)) μ-assoc : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ (liftFₛ (μₛ A))) ≋ (μₛ A ∘ μₛ (Delay≈ A))
μ-assoc {A} {x} = ∼⇒≈ (μ-assoc' {A} {x}) μ-assoc {A} {x} = ∼⇒≈ (μ-assoc' {A} {x})
identityˡ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay ∣ A ∣} {y : ∣ A ∣} → [ A ][ x ↓ y ] → [ A ][ ((μₛ A) ⟨$⟩ ((liftFₛ (ηₛ A)) ⟨$⟩ x)) ↓ y ] identityˡ↓ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay ∣ A ∣} {y : ∣ A ∣} → [ A ][ x ↓ y ] → [ A ][ ((μₛ A) ⟨$⟩ ((liftFₛ (ηₛ A)) ⟨$⟩ x)) ↓ y ]
@ -346,20 +346,20 @@ module DelayMonad where
identityˡ∼ {A} {later x} = later∼ identityˡ∼′ identityˡ∼ {A} {later x} = later∼ identityˡ∼′
force∼ (identityˡ∼′ {A} {x}) = identityˡ∼ force∼ (identityˡ∼′ {A} {x}) = identityˡ∼
identityˡ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ liftFₛ (ηₛ A)) ≋ idₛ (Delayₛ A) identityˡ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ liftFₛ (ηₛ A)) ≋ idₛ (Delay≈ A)
identityˡ′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay ∣ A ∣} → [ A ][ (μₛ A ∘ liftFₛ (ηₛ A)) ⟨$⟩ x ≈′ x ] identityˡ′ : ∀ {A : Setoid c (c ⊔ ℓ)} {x : Delay ∣ A ∣} → [ A ][ (μₛ A ∘ liftFₛ (ηₛ A)) ⟨$⟩ x ≈′ x ]
force≈ (identityˡ′ {A} {x}) = identityˡ force≈ (identityˡ′ {A} {x}) = identityˡ
identityˡ {A} {now x} = ≈-refl A identityˡ {A} {now x} = ≈-refl A
identityˡ {A} {later x} = later≈ identityˡ′ identityˡ {A} {later x} = later≈ identityˡ′
identityʳ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ ηₛ (Delayₛ A)) ≋ idₛ (Delayₛ A) identityʳ : ∀ {A : Setoid c (c ⊔ ℓ)} → (μₛ A ∘ ηₛ (Delay≈ A)) ≋ idₛ (Delay≈ A)
identityʳ {A} {now x} = ≈-refl A identityʳ {A} {now x} = ≈-refl A
identityʳ {A} {later x} = ≈-refl A identityʳ {A} {later x} = ≈-refl A
delayMonad : Monad (Setoids c (c ⊔ ℓ)) delayMonad : Monad (Setoids c (c ⊔ ℓ))
delayMonad = record delayMonad = record
{ F = record { F = record
{ F₀ = Delayₛ { F₀ = Delay≈
; F₁ = liftFₛ ; F₁ = liftFₛ
; identity = lift-id ; identity = lift-id
; homomorphism = λ {X} {Y} {Z} {f} {g} → lift-comp {X} {Y} {Z} {f} {g} ; homomorphism = λ {X} {Y} {Z} {f} {g} → lift-comp {X} {Y} {Z} {f} {g}
@ -433,7 +433,7 @@ module extra {A : Setoid c (c ⊔ ℓ)} where
ι (x , zero) = now x ι (x , zero) = now x
ι (x , suc n) = later (ι′ (x , n)) ι (x , suc n) = later (ι′ (x , n))
ιₛ' : (A ×ₛ (ℕ-setoid {c})) ⟶ Delayₛ∼ A ιₛ' : (A ×ₛ (ℕ-setoid {c})) ⟶ Delay∼ A
ιₛ' = record { to = ι ; cong = ι-cong } ιₛ' = record { to = ι ; cong = ι-cong }
where where
ι-cong : ∀ {x y} → [ A ×ₛ (ℕ-setoid {c}) ][ x ≡ y ] → [ A ][ ι x ∼ ι y ] ι-cong : ∀ {x y} → [ A ×ₛ (ℕ-setoid {c}) ][ x ≡ y ] → [ A ][ ι x ∼ ι y ]

142
agda/src/Monad/Instance/Setoids/K.lagda.md
View file

@ -76,8 +76,8 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
helper : [ Y ⊎ₛ X ][ inj₁ a ≡ inj₂ b ] helper : [ Y ⊎ₛ X ][ inj₁ a ≡ inj₂ b ]
helper rewrite (≣-sym fi₁) | (≣-sym fi₂) = cong f x≡y helper rewrite (≣-sym fi₁) | (≣-sym fi₂) = cong f x≡y
iter-cong∼ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ∼ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼ (iter {A} {X} < f > y) ] iter-cong∼ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delay∼ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼ (iter {A} {X} < f > y) ]
iter-cong∼′ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ∼ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼′ (iter {A} {X} < f > y) ] iter-cong∼′ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delay∼ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ∼′ (iter {A} {X} < f > y) ]
force∼ (iter-cong∼′ {A} {X} f {x} {y} x≡y) = iter-cong∼ f x≡y force∼ (iter-cong∼′ {A} {X} f {x} {y} x≡y) = iter-cong∼ f x≡y
iter-cong∼ {A} {X} f {x} {y} x≡y with < f > x in eqx | < f > y in eqy 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 = inj₁-helper f x≡y eqx eqy
@ -85,8 +85,8 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx ... | 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)) ... | inj₂ a | inj₂ b = later∼ (iter-cong∼′ {A} {X} f (inj₂-helper f x≡y eqx eqy))
iter-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ≈ (iter {A} {X} < f > y) ] iter-cong : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delay≈ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ≈ (iter {A} {X} < f > y) ]
iter-cong′ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delayₛ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ≈′ (iter {A} {X} < f > y) ] iter-cong′ : ∀ {A X : Setoid ℓ ℓ} (f : X ⟶ (Delay≈ A ⊎ₛ X)) {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ (iter {A} {X} < f > x) ≈′ (iter {A} {X} < f > y) ]
force≈ (iter-cong′ {A} {X} f {x} {y} x≡y) = iter-cong f x≡y force≈ (iter-cong′ {A} {X} f {x} {y} x≡y) = iter-cong f x≡y
iter-cong {A} {X} f {x} {y} x≡y with < f > x in eqx | < f > y in eqy 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 = inj₁-helper f x≡y eqx eqy
@ -94,43 +94,43 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
... | inj₂ a | inj₁ b = absurd-helper f (≡-sym X x≡y) eqy eqx ... | 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)) ... | inj₂ a | inj₂ b = later≈ (iter-cong′ {A} {X} f (inj₂-helper f x≡y eqx eqy))
iterₛ∼ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delayₛ∼ A ⊎ₛ X)) → X ⟶ Delayₛ∼ A iterₛ∼ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delay∼ A ⊎ₛ X)) → X ⟶ Delay∼ A
iterₛ∼ {A} {X} f = record { to = iter {A} {X} < f > ; cong = iter-cong∼ {A} {X} f } iterₛ∼ {A} {X} f = record { to = iter {A} {X} < f > ; cong = iter-cong∼ {A} {X} f }
iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delayₛ A ⊎ₛ X)) → X ⟶ Delayₛ A iterₛ : ∀ {A X : Setoid ℓ ℓ} → (X ⟶ (Delay≈ A ⊎ₛ X)) → X ⟶ Delay≈ A
iterₛ {A} {X} f = record { to = iter {A} {X} < f > ; cong = iter-cong {A} {X} f } iterₛ {A} {X} f = record { to = iter {A} {X} < f > ; cong = iter-cong {A} {X} f }
iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {x : ∣ X ∣} → [ A ][ iter {A} {X} < f > x ≈ [ Function.id , iter {A} {X} < f > ] (f ⟨$⟩ x) ] iter-fixpoint : ∀ {A X : Setoid ℓ ℓ} {f : X ⟶ (Delay≈ A ⊎ₛ X)} {x : ∣ X ∣} → [ A ][ iter {A} {X} < f > x ≈ [ Function.id , iter {A} {X} < f > ] (f ⟨$⟩ x) ]
iter-fixpoint {A} {X} {f} {x} with < f > x in eqx iter-fixpoint {A} {X} {f} {x} with < f > x in eqx
... | inj₁ a = ≈-refl A ... | inj₁ a = ≈-refl A
... | inj₂ a = ≈-trans A (≈-sym A later-self) (≈-refl A) ... | inj₂ a = ≈-trans A (≈-sym A later-self) (≈-refl A)
iter-resp-≈ : ∀ {A X : Setoid ℓ ℓ} (f g : X ⟶ (Delayₛ 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 : Setoid ℓ ℓ} (f g : X ⟶ (Delay≈ 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 : Setoid ℓ ℓ} (f g : X ⟶ (Delayₛ 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 : Setoid ℓ ℓ} (f g : X ⟶ (Delay≈ A ⊎ₛ X)) → f ≋ g → ∀ {x y : ∣ X ∣} → [ X ][ x ≡ y ] → [ A ][ iter {A} {X} < f > x ≈′ iter {A} {X} < g > y ]
force≈ (iter-resp-≈′ {A} {X} f g f≋g {x} {y} x≡y) = iter-resp-≈ f g f≋g {x} {y} x≡y force≈ (iter-resp-≈′ {A} {X} f g f≋g {x} {y} x≡y) = iter-resp-≈ f g f≋g {x} {y} x≡y
iter-resp-≈ {A} {X} f g f≋g {x} {y} x≡y with < f > x in eqa | < g > y in eqb iter-resp-≈ {A} {X} f g f≋g {x} {y} x≡y with < f > x in eqa | < g > y in eqb
... | inj₁ a | inj₁ b = drop-inj₁ helper ... | inj₁ a | inj₁ b = drop-inj₁ helper
where where
helper : [ Delayₛ A ⊎ₛ X ][ inj₁ a ≡ inj₁ b ] helper : [ Delay≈ A ⊎ₛ X ][ inj₁ a ≡ inj₁ b ]
helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delayₛ A ⊎ₛ X) (cong f x≡y) f≋g helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delay≈ A ⊎ₛ X) (cong f x≡y) f≋g
... | inj₁ a | inj₂ b = conflict (Delayₛ A) X helper ... | inj₁ a | inj₂ b = conflict (Delay≈ A) X helper
where where
helper : [ Delayₛ A ⊎ₛ X ][ inj₁ a ≡ inj₂ b ] helper : [ Delay≈ A ⊎ₛ X ][ inj₁ a ≡ inj₂ b ]
helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delayₛ A ⊎ₛ X) (cong f x≡y) f≋g helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delay≈ A ⊎ₛ X) (cong f x≡y) f≋g
... | inj₂ a | inj₁ b = conflict (Delayₛ A) X (≡-sym (Delayₛ A ⊎ₛ X) helper) ... | inj₂ a | inj₁ b = conflict (Delay≈ A) X (≡-sym (Delay≈ A ⊎ₛ X) helper)
where where
helper : [ Delayₛ A ⊎ₛ X ][ inj₂ a ≡ inj₁ b ] helper : [ Delay≈ A ⊎ₛ X ][ inj₂ a ≡ inj₁ b ]
helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delayₛ A ⊎ₛ X) (cong f x≡y) f≋g helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delay≈ A ⊎ₛ X) (cong f x≡y) f≋g
... | inj₂ a | inj₂ b = later≈ (iter-resp-≈′ f g f≋g (drop-inj₂ helper)) ... | inj₂ a | inj₂ b = later≈ (iter-resp-≈′ f g f≋g (drop-inj₂ helper))
where where
helper : [ Delayₛ A ⊎ₛ X ][ inj₂ a ≡ inj₂ b ] helper : [ Delay≈ A ⊎ₛ X ][ inj₂ a ≡ inj₂ b ]
helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delayₛ A ⊎ₛ X) (cong f x≡y) f≋g helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delay≈ A ⊎ₛ X) (cong f x≡y) f≋g
iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {g : Y ⟶ (Delayₛ A ⊎ₛ Y)} {h : X ⟶ Y} iter-uni : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delay≈ A ⊎ₛ X)} {g : Y ⟶ (Delay≈ A ⊎ₛ Y)} {h : X ⟶ Y}
→ ([ inj₁ₛ ∘ (idₛ (Delayₛ A)) , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ([ inj₁ₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h)
→ ∀ {x : ∣ X ∣} {y : ∣ Y ∣} → [ Y ][ y ≡ h ⟨$⟩ x ] → [ A ][ iter {A} {X} < f > x ≈ (iter {A} {Y} < g >) y ] → ∀ {x : ∣ X ∣} {y : ∣ Y ∣} → [ Y ][ y ≡ h ⟨$⟩ x ] → [ A ][ iter {A} {X} < f > x ≈ (iter {A} {Y} < g >) y ]
iter-uni′ : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {g : Y ⟶ (Delayₛ A ⊎ₛ Y)} {h : X ⟶ Y} iter-uni′ : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delay≈ A ⊎ₛ X)} {g : Y ⟶ (Delay≈ A ⊎ₛ Y)} {h : X ⟶ Y}
→ ([ inj₁ₛ ∘ (idₛ (Delayₛ A)) , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) → ([ inj₁ₛ , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h)
→ ∀ {x : ∣ X ∣} {y : ∣ Y ∣} → [ Y ][ y ≡ h ⟨$⟩ x ] → [ A ][ iter {A} {X} < f > x ≈′ (iter {A} {Y} < g >) y ] → ∀ {x : ∣ X ∣} {y : ∣ Y ∣} → [ Y ][ y ≡ h ⟨$⟩ x ] → [ A ][ iter {A} {X} < f > x ≈′ (iter {A} {Y} < g >) y ]
force≈ (iter-uni′ {A} {X} {Y} {f} {g} {h} eq {x} {y} y≡h$x) = iter-uni {A} {X} {Y} {f} {g} {h} eq {x} {y} y≡h$x force≈ (iter-uni′ {A} {X} {Y} {f} {g} {h} eq {x} {y} y≡h$x) = iter-uni {A} {X} {Y} {f} {g} {h} eq {x} {y} y≡h$x
iter-uni {A} {X} {Y} {f} {g} {h} eq {x} {y} x≡y with f ⟨$⟩ x in eqx | g ⟨$⟩ (h ⟨$⟩ x) in eqy | g ⟨$⟩ y in eqz | eq {x} iter-uni {A} {X} {Y} {f} {g} {h} eq {x} {y} x≡y with f ⟨$⟩ x in eqx | g ⟨$⟩ (h ⟨$⟩ x) in eqy | g ⟨$⟩ y in eqz | eq {x}
@ -140,10 +140,10 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
... | inj₂ a | inj₂ b | inj₂ c | inj₂ req = later≈ (iter-uni′ {f = f} {g = g}{h = h} eq c≡h$a) ... | inj₂ a | inj₂ b | inj₂ c | inj₂ req = later≈ (iter-uni′ {f = f} {g = g}{h = h} eq c≡h$a)
where where
c≡h$a : [ Y ][ c ≡ h ⟨$⟩ a ] c≡h$a : [ Y ][ c ≡ h ⟨$⟩ a ]
c≡h$a = ≡-trans Y (drop-inj₂ (≡-trans (Delayₛ A ⊎ₛ Y) (≡-trans (Delayₛ A ⊎ₛ Y) (≡-sym (Delayₛ A ⊎ₛ Y) (≡→≡ {Delayₛ A ⊎ₛ Y} eqz)) (cong g x≡y)) (≡→≡ {Delayₛ A ⊎ₛ Y} eqy))) (≡-sym Y req) c≡h$a = ≡-trans Y (drop-inj₂ (≡-trans (Delay≈ A ⊎ₛ Y) (≡-trans (Delay≈ A ⊎ₛ Y) (≡-sym (Delay≈ A ⊎ₛ Y) (≡→≡ {Delay≈ A ⊎ₛ Y} eqz)) (cong g x≡y)) (≡→≡ {Delay≈ A ⊎ₛ Y} eqy))) (≡-sym Y req)
iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ (X ⊎ₛ Y)} {x : ∣ 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 >) ] x ] iter-folding : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delay≈ A ⊎ₛ X)} {h : Y ⟶ (X ⊎ₛ Y)} {x : ∣ 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 >) ] x ]
iter-folding′ : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delayₛ A ⊎ₛ X)} {h : Y ⟶ (X ⊎ₛ Y)} {x : ∣ 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 >) ] x ] iter-folding′ : ∀ {A X Y : Setoid ℓ ℓ} {f : X ⟶ (Delay≈ A ⊎ₛ X)} {h : Y ⟶ (X ⊎ₛ Y)} {x : ∣ 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 >) ] x ]
force≈ (iter-folding′ {A} {X} {Y} {f} {h} {x}) = iter-folding {A} {X} {Y} {f} {h} {x} force≈ (iter-folding′ {A} {X} {Y} {f} {h} {x}) = iter-folding {A} {X} {Y} {f} {h} {x}
iter-folding {A} {X} {Y} {f} {h} {inj₁ x} with f ⟨$⟩ x in eqa iter-folding {A} {X} {Y} {f} {h} {inj₁ x} with f ⟨$⟩ x in eqa
... | inj₁ a = ≈-refl A ... | inj₁ a = ≈-refl A
@ -159,7 +159,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
... | inj₁ a = later≈ (iter-folding′ {A} {X} {Y} {f} {h} {inj₁ a}) ... | inj₁ a = later≈ (iter-folding′ {A} {X} {Y} {f} {h} {inj₁ a})
... | inj₂ a = later≈ (iter-folding′ {A} {X} {Y} {f} {h} {inj₂ a}) ... | inj₂ a = later≈ (iter-folding′ {A} {X} {Y} {f} {h} {inj₂ a})
delay-algebras-on : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (Delayₛ A) delay-algebras-on : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (Delay≈ A)
delay-algebras-on {A} = record delay-algebras-on {A} = record
{ _# = iterₛ {A} { _# = iterₛ {A}
; #-Fixpoint = λ {X} {f} → iter-fixpoint {A} {X} {f} ; #-Fixpoint = λ {X} {f} → iter-fixpoint {A} {X} {f}
@ -169,7 +169,7 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
} }
delay-algebras : ∀ (A : Setoid ℓ ℓ) → Elgot-Algebra delay-algebras : ∀ (A : Setoid ℓ ℓ) → Elgot-Algebra
delay-algebras A = record { A = Delayₛ A ; algebra = delay-algebras-on {A}} delay-algebras A = record { A = Delay≈ A ; algebra = delay-algebras-on {A}}
open Elgot-Algebra using (#-Fixpoint; #-Uniformity; #-Compositionality; #-resp-≈; #-Diamond) renaming (A to ⟦_⟧) open Elgot-Algebra using (#-Fixpoint; #-Uniformity; #-Compositionality; #-resp-≈; #-Diamond) renaming (A to ⟦_⟧)
@ -183,12 +183,12 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
helper₁ (now x) = inj₁ (< f > x) helper₁ (now x) = inj₁ (< f > x)
helper₁ (later x) = inj₂ (force x) helper₁ (later x) = inj₂ (force x)
helper₁-cong : {x y : Delay ∣ A ∣} → (x∼y : [ A ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ helper₁ x ≡ helper₁ y ] helper₁-cong : {x y : Delay ∣ A ∣} → (x∼y : [ A ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delay∼ A ][ helper₁ x ≡ helper₁ y ]
helper₁-cong (now∼ x≡y) = inj₁ (cong f x≡y) helper₁-cong (now∼ x≡y) = inj₁ (cong f x≡y)
helper₁-cong (later∼ x≡y) = inj₂ (force∼ x≡y) helper₁-cong (later∼ x≡y) = inj₂ (force∼ x≡y)
-- -- setoid-morphism that preserves strong-bisimilarity -- -- setoid-morphism that preserves strong-bisimilarity
helper : (Delayₛ∼ A) ⟶ (⟦ B ⟧ ⊎ₛ Delayₛ∼ A) helper : (Delay∼ A) ⟶ (⟦ B ⟧ ⊎ₛ Delay∼ A)
helper = record { to = helper₁ ; cong = helper₁-cong} helper = record { to = helper₁ ; cong = helper₁-cong}
helper#∼-cong : {x y : Delay ∣ A ∣} → (x∼y : [ A ][ x ∼ y ]) → [ ⟦ B ⟧ ][ helper # ⟨$⟩ x ≡ helper # ⟨$⟩ y ] helper#∼-cong : {x y : Delay ∣ A ∣} → (x∼y : [ A ][ x ∼ y ]) → [ ⟦ B ⟧ ][ helper # ⟨$⟩ x ≡ helper # ⟨$⟩ y ]
@ -223,31 +223,31 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
helper₁' (now (x , suc n)) = inj₂ (< liftFₛ∼ outer > (ι {A} (x , n))) helper₁' (now (x , suc n)) = inj₂ (< liftFₛ∼ outer > (ι {A} (x , n)))
helper₁' (later y) = inj₂ (force y) helper₁' (later y) = inj₂ (force y)
helper₁-cong' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid) ][ helper₁' x ≡ helper₁' y ] helper₁-cong' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid) ][ helper₁' x ≡ helper₁' y ]
helper₁-cong' {now (x , zero)} (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y) helper₁-cong' {now (x , zero)} (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y)
helper₁-cong' {now (x , suc n)} {now (y , suc _)} (now∼ (x≡y , ≣-refl)) = inj₂ (cong (liftFₛ∼ outer) (cong ιₛ' (x≡y , ≣-refl))) helper₁-cong' {now (x , suc n)} {now (y , suc _)} (now∼ (x≡y , ≣-refl)) = inj₂ (cong (liftFₛ∼ outer) (cong ιₛ' (x≡y , ≣-refl)))
helper₁-cong' (later∼ x∼y) = inj₂ (force∼ x∼y) helper₁-cong' (later∼ x∼y) = inj₂ (force∼ x∼y)
helper' : (Delayₛ∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)) helper' : (Delay∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid))
helper' = record { to = helper₁' ; cong = helper₁-cong'} helper' = record { to = helper₁' ; cong = helper₁-cong'}
helper₁'' : Delay (∣ A ∣ × ℕ {ℓ}) → ∣ ⟦ B ⟧ ∣ ⊎ Delay (∣ A ∣ × ℕ {ℓ}) helper₁'' : Delay (∣ A ∣ × ℕ {ℓ}) → ∣ ⟦ B ⟧ ∣ ⊎ Delay (∣ A ∣ × ℕ {ℓ})
helper₁'' (now (x , _)) = inj₁ (< f > x) helper₁'' (now (x , _)) = inj₁ (< f > x)
helper₁'' (later y) = inj₂ (force y) helper₁'' (later y) = inj₂ (force y)
helper₁-cong'' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid) ][ helper₁'' x ≡ helper₁'' y ] helper₁-cong'' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid) ][ helper₁'' x ≡ helper₁'' y ]
helper₁-cong'' {now (x , _)} (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y) helper₁-cong'' {now (x , _)} (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y)
helper₁-cong'' (later∼ x∼y) = inj₂ (force∼ x∼y) helper₁-cong'' (later∼ x∼y) = inj₂ (force∼ x∼y)
helper'' : (Delayₛ∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)) helper'' : (Delay∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid))
helper'' = record { to = helper₁'' ; cong = helper₁-cong''} helper'' = record { to = helper₁'' ; cong = helper₁-cong''}
-- Needs #-Diamond -- Needs #-Diamond
eq₀ : ∀ {z} → [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper'' # ⟨$⟩ z ] eq₀ : ∀ {z} → [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper'' # ⟨$⟩ z ]
eq₀ {z} = ≡-trans ⟦ B ⟧ eq₀ {z} = ≡-trans ⟦ B ⟧
(#-resp-≈ B {Delayₛ∼ (A ×ₛ ℕ-setoid)} {helper'} step₁) (#-resp-≈ B {Delay∼ (A ×ₛ ℕ-setoid)} {helper'} step₁)
(≡-trans ⟦ B ⟧ (≡-trans ⟦ B ⟧
(#-Diamond B {Delayₛ∼ (A ×ₛ ℕ-setoid)} helper''') (#-Diamond B {Delay∼ (A ×ₛ ℕ-setoid)} helper''')
(#-resp-≈ B (λ {x} → (step₂ {x})))) (#-resp-≈ B (λ {x} → (step₂ {x}))))
where where
helper₁''' : Delay (∣ A ∣ × ℕ {ℓ}) → ∣ ⟦ B ⟧ ∣ ⊎ (Delay (∣ A ∣ × ℕ {ℓ}) ⊎ Delay (∣ A ∣ × ℕ {ℓ})) helper₁''' : Delay (∣ A ∣ × ℕ {ℓ}) → ∣ ⟦ B ⟧ ∣ ⊎ (Delay (∣ A ∣ × ℕ {ℓ}) ⊎ Delay (∣ A ∣ × ℕ {ℓ}))
@ -255,45 +255,45 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
helper₁''' (now (x , suc n)) = inj₂ (inj₁ (< liftFₛ∼ outer > (ι {A} (x , n)))) helper₁''' (now (x , suc n)) = inj₂ (inj₁ (< liftFₛ∼ outer > (ι {A} (x , n))))
helper₁''' (later y) = inj₂ (inj₂ (force y)) helper₁''' (later y) = inj₂ (inj₂ (force y))
helper₁-cong''' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ (Delayₛ∼ (A ×ₛ ℕ-setoid) ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)) ][ helper₁''' x ≡ helper₁''' y ] helper₁-cong''' : {x y : Delay (∣ A ∣ × ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ (Delay∼ (A ×ₛ ℕ-setoid) ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid)) ][ helper₁''' x ≡ helper₁''' y ]
helper₁-cong''' {now (x , zero)} (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y) helper₁-cong''' {now (x , zero)} (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y)
helper₁-cong''' {now (x , suc n)} {now (y , suc _)} (now∼ (x≡y , ≣-refl)) = inj₂ (inj₁ (cong (liftFₛ∼ outer) (cong ιₛ' (x≡y , ≣-refl)))) helper₁-cong''' {now (x , suc n)} {now (y , suc _)} (now∼ (x≡y , ≣-refl)) = inj₂ (inj₁ (cong (liftFₛ∼ outer) (cong ιₛ' (x≡y , ≣-refl))))
helper₁-cong''' (later∼ x∼y) = inj₂ (inj₂ (force∼ x∼y)) helper₁-cong''' (later∼ x∼y) = inj₂ (inj₂ (force∼ x∼y))
helper''' : (Delayₛ∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ (Delayₛ∼ (A ×ₛ ℕ-setoid) ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid))) helper''' : (Delay∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ (Delay∼ (A ×ₛ ℕ-setoid) ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid)))
helper''' = record { to = helper₁''' ; cong = helper₁-cong''' } helper''' = record { to = helper₁''' ; cong = helper₁-cong''' }
step₁ : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid) ][ helper' ⟨$⟩ x ≡ ([ inj₁ , inj₂ ∘′ [ id , id ] ] ∘′ helper₁''') x ] step₁ : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid) ][ helper' ⟨$⟩ x ≡ ([ inj₁ , inj₂ ∘′ [ id , id ] ] ∘′ helper₁''') x ]
step₁ {now (a , zero)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)) step₁ {now (a , zero)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid))
step₁ {now (a , suc n)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)) step₁ {now (a , suc n)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid))
step₁ {later x} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)) step₁ {later x} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid))
step₂ : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid) ][ ([ inj₁ , [ inj₁ ∘′ < ([ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delayₛ∼ (A ×ₛ ℕ-setoid)) , idₛ (Delayₛ∼ (A ×ₛ ℕ-setoid)) ]ₛ ]ₛ ∘ helper''') # > , inj₂ ] ] ∘′ helper₁''') x ≡ helper'' ⟨$⟩ x ] step₂ : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid) ][ ([ inj₁ , [ inj₁ ∘′ < ([ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delay∼ (A ×ₛ ℕ-setoid)) , idₛ (Delay∼ (A ×ₛ ℕ-setoid)) ]ₛ ]ₛ ∘ helper''') # > , inj₂ ] ] ∘′ helper₁''') x ≡ helper'' ⟨$⟩ x ]
step₂ {now (a , zero)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)) step₂ {now (a , zero)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid))
step₂ {now (x , suc n)} = inj₁ (by-induction n) step₂ {now (x , suc n)} = inj₁ (by-induction n)
where where
by-induction : ∀ n → [ ⟦ B ⟧ ][ < ([ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delayₛ∼ (A ×ₛ ℕ-setoid)) , idₛ (Delayₛ∼ (A ×ₛ ℕ-setoid)) ]ₛ ]ₛ ∘ helper''') # > (< liftFₛ∼ outer > (ι (x , n))) ≡ f ⟨$⟩ x ] by-induction : ∀ n → [ ⟦ B ⟧ ][ < ([ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delay∼ (A ×ₛ ℕ-setoid)) , idₛ (Delay∼ (A ×ₛ ℕ-setoid)) ]ₛ ]ₛ ∘ helper''') # > (< liftFₛ∼ outer > (ι (x , n))) ≡ f ⟨$⟩ x ]
by-induction zero = #-Fixpoint B by-induction zero = #-Fixpoint B
by-induction (suc n) = ≡-trans ⟦ B ⟧ (#-Fixpoint B) (by-induction n) by-induction (suc n) = ≡-trans ⟦ B ⟧ (#-Fixpoint B) (by-induction n)
step₂ {later y} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)) step₂ {later y} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid))
eq₁ : ∀ {z} → [ ⟦ B ⟧ ][ helper'' # ⟨$⟩ z ≡ helper # ⟨$⟩ liftF proj₁ z ] eq₁ : ∀ {z} → [ ⟦ B ⟧ ][ helper'' # ⟨$⟩ z ≡ helper # ⟨$⟩ liftF proj₁ z ]
eq₁ {z} = #-Uniformity B {f = helper''} {g = helper} {h = liftFₛ∼ proj₁ₛ} by-uni eq₁ {z} = #-Uniformity B {f = helper''} {g = helper} {h = liftFₛ∼ proj₁ₛ} by-uni
where where
by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ [ inj₁ , inj₂ ∘′ (liftF proj₁) ] (helper₁'' x) ≡ (< helper > ∘′ liftF proj₁) x ] by-uni : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delay∼ A ][ [ inj₁ , inj₂ ∘′ (liftF proj₁) ] (helper₁'' x) ≡ (< helper > ∘′ liftF proj₁) x ]
by-uni {now (a , b)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ A) by-uni {now (a , b)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼ A)
by-uni {later x} = ≡-refl (⟦ B ⟧ ⊎ₛ Delayₛ∼ A) by-uni {later x} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼ A)
eq : ∀ {x y} → [ A ×ₛ ℕ-setoid ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' x) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) y ] eq : ∀ {x y} → [ A ×ₛ ℕ-setoid ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delay∼ A ][ [ inj₁ , inj₂ ∘′ μ ∘′ (liftF ι) ] (helper₁' x) ≡ (helper₁ ∘′ μ ∘′ (liftF ι)) y ]
eq {now (x , n)} {now (y , .n)} (now∼ (x∼y , ≣-refl)) = eq' {n} eq {now (x , n)} {now (y , .n)} (now∼ (x∼y , ≣-refl)) = eq' {n}
where where
eq' : ∀ {n} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ [ inj₁ , inj₂ ∘′ μ ∘′ liftF ι ] (helper₁' (now (x , n))) ≡ (helper₁ ∘′ μ {A} ∘′ liftF ι) (now (y , n)) ] eq' : ∀ {n} → [ ⟦ B ⟧ ⊎ₛ Delay∼ A ][ [ inj₁ , inj₂ ∘′ μ ∘′ liftF ι ] (helper₁' (now (x , n))) ≡ (helper₁ ∘′ μ {A} ∘′ liftF ι) (now (y , n)) ]
eq' {zero} = inj₁ (cong f x∼y) eq' {zero} = inj₁ (cong f x∼y)
eq' {suc n} = inj₂ (∼-trans A (cong (μₛ∼ A) (∼-sym (Delayₛ∼ A) (lift-comp∼ {f = outer} {g = ιₛ'} {ι (x , n)} (∼-refl A)))) (∼-trans A identityˡ∼ (cong ιₛ' (x∼y , ≣-refl)))) eq' {suc n} = inj₂ (∼-trans A (cong (μₛ∼ A) (∼-sym (Delay∼ A) (lift-comp∼ {f = outer} {g = ιₛ'} {ι (x , n)} (∼-refl A)))) (∼-trans A identityˡ∼ (cong ιₛ' (x∼y , ≣-refl))))
eq (later∼ x∼y) = inj₂ (cong (μₛ∼ A) (cong (liftFₛ∼ ιₛ') (force∼ x∼y))) eq (later∼ x∼y) = inj₂ (cong (μₛ∼ A) (cong (liftFₛ∼ ιₛ') (force∼ x∼y)))
eq₂ : [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z)] eq₂ : [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z)]
eq₂ = Elgot-Algebra.#-Uniformity B {Delayₛ∼ (A ×ₛ ℕ-setoid {ℓ})} {Delayₛ∼ A} {helper'} {helper} {μₛ∼ A ∘ liftFₛ∼ ιₛ'} (λ {x} → eq {x} {x} (∼-refl (A ×ₛ ℕ-setoid))) eq₂ = Elgot-Algebra.#-Uniformity B {Delay∼ (A ×ₛ ℕ-setoid {ℓ})} {Delay∼ A} {helper'} {helper} {μₛ∼ A ∘ liftFₛ∼ ιₛ'} (λ {x} → eq {x} {x} (∼-refl (A ×ₛ ℕ-setoid)))
delay-lift' = record { to = < helper # > ; cong = helper#≈-cong } delay-lift' = record { to = < helper # > ; cong = helper#≈-cong }
@ -307,34 +307,34 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
_⟶_.to ‖‖-quote x = x _⟶_.to ‖‖-quote x = x
cong (‖‖-quote {X}) ≣-refl = ≡-refl X cong (‖‖-quote {X}) ≣-refl = ≡-refl X
disc-dom : ∀ {X : Setoid ℓ ℓ} → X ⟶ (Delayₛ A ⊎ₛ X) → ‖ X ‖ ⟶ (Delayₛ∼ A ⊎ₛ ‖ X ‖) disc-dom : ∀ {X : Setoid ℓ ℓ} → X ⟶ (Delay≈ A ⊎ₛ X) → ‖ X ‖ ⟶ (Delay∼ A ⊎ₛ ‖ X ‖)
_⟶_.to (disc-dom f) x = f ⟨$⟩ x _⟶_.to (disc-dom f) x = f ⟨$⟩ x
cong (disc-dom {X} f) {x} {y} x≡y rewrite x≡y = ≡-refl (Delayₛ∼ A ⊎ₛ ‖ X ‖) cong (disc-dom {X} f) {x} {y} x≡y rewrite x≡y = ≡-refl (Delay∼ A ⊎ₛ ‖ X ‖)
iter-g-var : ∀ {X : Setoid ℓ ℓ} → (g : X ⟶ (Delayₛ A ⊎ₛ X)) → ∀ {x} → [ A ][ (iter {A} {X} < g >) x ∼ (iterₛ∼ {A} {‖ X ‖} (disc-dom g)) ⟨$⟩ x ] iter-g-var : ∀ {X : Setoid ℓ ℓ} → (g : X ⟶ (Delay≈ A ⊎ₛ X)) → ∀ {x} → [ A ][ (iter {A} {X} < g >) x ∼ (iterₛ∼ {A} {‖ X ‖} (disc-dom g)) ⟨$⟩ x ]
iter-g-var′ : ∀ {X : Setoid ℓ ℓ} → (g : X ⟶ (Delayₛ A ⊎ₛ X)) → ∀ {x} → [ A ][ (iter {A} {X} < g >) x ∼′ (iterₛ∼ {A} {‖ X ‖} (disc-dom g)) ⟨$⟩ x ] iter-g-var′ : ∀ {X : Setoid ℓ ℓ} → (g : X ⟶ (Delay≈ A ⊎ₛ X)) → ∀ {x} → [ A ][ (iter {A} {X} < g >) x ∼′ (iterₛ∼ {A} {‖ X ‖} (disc-dom g)) ⟨$⟩ x ]
force∼ (iter-g-var′ {X} g {x}) = iter-g-var {X} g {x} force∼ (iter-g-var′ {X} g {x}) = iter-g-var {X} g {x}
iter-g-var {X} g {x} with g ⟨$⟩ x iter-g-var {X} g {x} with g ⟨$⟩ x
... | inj₁ a = ∼-refl A ... | inj₁ a = ∼-refl A
... | inj₂ a = later∼ (iter-g-var′ {X} g {a}) ... | inj₂ a = later∼ (iter-g-var′ {X} g {a})
preserves' : ∀ {X : Setoid ℓ ℓ} {g : X ⟶ (Delayₛ A ⊎ₛ X)} → ∀ {x} → [ ⟦ B ⟧ ][ (delay-lift' ∘ (iterₛ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ] preserves' : ∀ {X : Setoid ℓ ℓ} {g : X ⟶ (Delay≈ A ⊎ₛ X)} → ∀ {x} → [ ⟦ B ⟧ ][ (delay-lift' ∘ (iterₛ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ]
preserves' {X} {g} {x} = ≡-trans ⟦ B ⟧ step₁ step₂ preserves' {X} {g} {x} = ≡-trans ⟦ B ⟧ step₁ step₂
where where
step₁ : [ ⟦ B ⟧ ][ (delay-lift' ∘ (iterₛ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ] step₁ : [ ⟦ B ⟧ ][ (delay-lift' ∘ (iterₛ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ]
step₁ = ≡-trans ⟦ B ⟧ (≡-trans ⟦ B ⟧ (helper#∼-cong (iter-g-var g)) (sub-step₁ (disc-dom g) {inj₂ x})) (≡-sym ⟦ B ⟧ (#-Compositionality B {f = helper} {h = disc-dom g})) step₁ = ≡-trans ⟦ B ⟧ (≡-trans ⟦ B ⟧ (helper#∼-cong (iter-g-var g)) (sub-step₁ (disc-dom g) {inj₂ x})) (≡-sym ⟦ B ⟧ (#-Compositionality B {f = helper} {h = disc-dom g}))
where where
sub-step₁ : (g : ‖ X ‖ ⟶ ((Delayₛ∼ A) ⊎ₛ ‖ X ‖)) → ∀ {x} → [ ⟦ B ⟧ ][ ((helper #) ∘ [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ) ⟨$⟩ x sub-step₁ : (g : ‖ X ‖ ⟶ ((Delay∼ A) ⊎ₛ ‖ X ‖)) → ∀ {x} → [ ⟦ B ⟧ ][ ((helper #) ∘ [ idₛ (Delay∼ A) , iterₛ∼ g ]ₛ) ⟨$⟩ x
≡ ([ [ inj₁ₛ , inj₂ₛ ∘ inj₁ₛ ]ₛ ∘ helper , inj₂ₛ ∘ inj₂ₛ ]ₛ ∘ [ inj₁ₛ , g ]ₛ) # ⟨$⟩ x ] ≡ ([ [ inj₁ₛ , inj₂ₛ ∘ inj₁ₛ ]ₛ ∘ helper , inj₂ₛ ∘ inj₂ₛ ]ₛ ∘ [ inj₁ₛ , g ]ₛ) # ⟨$⟩ x ]
sub-step₁ g {u} = ≡-sym ⟦ B ⟧ (#-Uniformity B {h = [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ} (λ {y} → last-step {y})) sub-step₁ g {u} = ≡-sym ⟦ B ⟧ (#-Uniformity B {h = [ idₛ (Delay∼ A) , iterₛ∼ g ]ₛ} (λ {y} → last-step {y}))
where where
last-step : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ (Delayₛ∼ A) ][ [ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ ]ₛ ∘ [ [ inj₁ₛ , inj₂ₛ ∘ inj₁ₛ ]ₛ ∘ helper , inj₂ₛ ∘ inj₂ₛ ]ₛ ∘ [ inj₁ₛ , g ]ₛ ⟨$⟩ x ≡ (helper ∘ [ idₛ (Delayₛ∼ A) , iterₛ∼ g ]ₛ) ⟨$⟩ x ] last-step : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ (Delay∼ A) ][ [ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delay∼ A) , iterₛ∼ g ]ₛ ]ₛ ∘ [ [ inj₁ₛ , inj₂ₛ ∘ inj₁ₛ ]ₛ ∘ helper , inj₂ₛ ∘ inj₂ₛ ]ₛ ∘ [ inj₁ₛ , g ]ₛ ⟨$⟩ x ≡ (helper ∘ [ idₛ (Delay∼ A) , iterₛ∼ g ]ₛ) ⟨$⟩ x ]
last-step {inj₁ (now a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A)) last-step {inj₁ (now a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼ A))
last-step {inj₁ (later a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A)) last-step {inj₁ (later a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼ A))
last-step {inj₂ a} with g ⟨$⟩ a in eqb last-step {inj₂ a} with g ⟨$⟩ a in eqb
... | inj₁ (now b) = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A)) ... | inj₁ (now b) = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼ A))
... | inj₁ (later b) = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A)) ... | inj₁ (later b) = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼ A))
... | inj₂ b = ≡-refl (⟦ B ⟧ ⊎ₛ (Delayₛ∼ A)) ... | inj₂ b = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼ A))
step₂ : [ ⟦ B ⟧ ][ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ] step₂ : [ ⟦ B ⟧ ][ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift' , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ]
step₂ = #-Uniformity B {h = ‖‖-quote} sub-step₂ step₂ = #-Uniformity B {h = ‖‖-quote} sub-step₂
where where
@ -359,23 +359,23 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
→ (<< h >> ∘ (ηₛ A)) ≋ f → (<< h >> ∘ (ηₛ A)) ≋ f
→ << g >> ≋ << h >> → << g >> ≋ << h >>
*-uniq' {B} f g h eqᵍ eqʰ {x} = ≡-trans ⟦ B ⟧ (cong << g >> iter-id) *-uniq' {B} f g h eqᵍ eqʰ {x} = ≡-trans ⟦ B ⟧ (cong << g >> iter-id)
(≡-trans ⟦ B ⟧ (preserves g {Delayₛ∼ A} {[ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now} {x = x}) (≡-trans ⟦ B ⟧ (preserves g {Delay∼ A} {[ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now} {x = x})
(≡-trans ⟦ B ⟧ (#-resp-≈ B (λ {x} → helper-eq' {x}) {x}) (≡-trans ⟦ B ⟧ (#-resp-≈ B (λ {x} → helper-eq' {x}) {x})
(≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ (preserves h {Delayₛ∼ A} {[ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now} {x = x})) (≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ (preserves h {Delay∼ A} {[ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now} {x = x}))
(≡-sym ⟦ B ⟧ (cong << h >> iter-id))))) (≡-sym ⟦ B ⟧ (cong << h >> iter-id)))))
where where
open Elgot-Algebra B using (_#) open Elgot-Algebra B using (_#)
D∼⇒D≈ : ∀ {A : Setoid ℓ ℓ} → Delayₛ∼ A ⟶ Delayₛ A D∼⇒D≈ : ∀ {A : Setoid ℓ ℓ} → Delay∼ A ⟶ Delay≈ A
D∼⇒D≈ {A} = record { to = λ x → x ; cong = λ eq → ∼⇒≈ eq } D∼⇒D≈ {A} = record { to = λ x → x ; cong = λ eq → ∼⇒≈ eq }
helper-now₁ : (Delay ∣ A ∣) → (Delay ∣ A ∣ ⊎ (Delay ∣ A ∣)) helper-now₁ : (Delay ∣ A ∣) → (Delay ∣ A ∣ ⊎ (Delay ∣ A ∣))
helper-now₁ (now x) = inj₁ (now x) helper-now₁ (now x) = inj₁ (now x)
helper-now₁ (later x) = inj₂ (force x) helper-now₁ (later x) = inj₂ (force x)
helper-now : Delayₛ∼ A ⟶ ((Delayₛ∼ A) ⊎ₛ (Delayₛ∼ A)) helper-now : Delay∼ A ⟶ ((Delay∼ A) ⊎ₛ (Delay∼ A))
helper-now = record { to = helper-now₁ ; cong = λ { (now∼ eq) → inj₁ (now∼ eq) helper-now = record { to = helper-now₁ ; cong = λ { (now∼ eq) → inj₁ (now∼ eq)
; (later∼ eq) → inj₂ (force∼ eq) } } ; (later∼ eq) → inj₂ (force∼ eq) } }
helper-eq' : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delayₛ∼ A ][ ([ inj₁ₛ ∘ << g >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x helper-eq' : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ Delay∼ A ][ ([ inj₁ₛ ∘ << g >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x
≡ ([ inj₁ₛ ∘ << h >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ] ≡ ([ inj₁ₛ ∘ << h >> , inj₂ₛ ]ₛ ∘ [ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
helper-eq' {now x} = inj₁ (≡-trans ⟦ B ⟧ eqᵍ (≡-sym ⟦ B ⟧ eqʰ)) helper-eq' {now x} = inj₁ (≡-trans ⟦ B ⟧ eqᵍ (≡-sym ⟦ B ⟧ eqʰ))
helper-eq' {later x} = inj₂ (∼-refl A) helper-eq' {later x} = inj₂ (∼-refl A)

2
thesis/src/04_iteration.tex
View file

@ -152,7 +152,7 @@ We will usually refer to right-stable free Elgot algebras as just stable Elgot a
Stability of $KX$ expresses that it somehow behaves like it would in a cartesian closed category, the following theorem should then follow trivially: Stability of $KX$ expresses that it somehow behaves like it would in a cartesian closed category, the following theorem should then follow trivially:
\begin{theorem} \begin{theorem}\label{thm:stability}
In a cartesian closed category every free Elgot algebra is stable. In a cartesian closed category every free Elgot algebra is stable.
\end{theorem} \end{theorem}
\begin{proof} \begin{proof}

59
thesis/src/05_setoids.tex
View file

@ -19,6 +19,7 @@ Morphisms between setoids are functions that respect the equivalence relation:
Setoids and setoid morphisms form a category that we call $\setoids$. Setoids and setoid morphisms form a category that we call $\setoids$.
\improvement[inline]{Text is not good} \improvement[inline]{Text is not good}
\todo[inline]{sketch the proof that setoids is CCC and cocartesian}
\section{Quotienting the Delay Monad} \section{Quotienting the Delay Monad}
@ -34,7 +35,7 @@ codata (A : Set) : Set where
later : Delay A → Delay A later : Delay A → Delay A
\end{minted} \end{minted}
This style is sometimes called \textit{positively coinductive} and is nowadays advised against in the manuals of both Agda and Coq\todo{cite}. Instead one is advised to use coinductive records, we will heed this advice and use the following representation of the delay monad: This style is sometimes called \textit{positively coinductive} and is nowadays advised against in the manuals of both Agda and Coq\todo{cite}. Instead one is advised to use coinductive records, we will heed this advice and use the following representation of the delay monad in Agda:
\todo[inline]{cite https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html somehow} \todo[inline]{cite https://www.cse.chalmers.se/~nad/listings/delay-monad/Delay-monad.html somehow}
@ -70,7 +71,7 @@ We will now introduce two notions of equality on inhabitants of the delay type,
$(Delay\;A, \sim)$ is a setoid. $(Delay\;A, \sim)$ is a setoid.
\end{lemma} \end{lemma}
In $(Delay\;A, \sim)$ computations with different execution time but the same result are not equal. We will now quotient this type by weak bisimilarity, i.e. we will identify all computations that terminate with the same result. Let us first consider what it means for a computation to evaluate to some result: In $(Delay\;A, \sim)$ computations that evaluate to the same result but in a different amount of time are not equal. We will now quotient this type by weak bisimilarity, i.e. we will identify all computations that terminate with the same result. Let us first consider what it means for a computation to evaluate to some result:
\[ \[
\inferrule*{eq : x =^A y}{now\; eq : now\;x \downarrow y} \hskip 1cm \inferrule*{eq : x =^A y}{now\; eq : now\;x \downarrow y} \hskip 1cm
@ -102,9 +103,57 @@ Now we can relate two computations \textit{iff} they evaluate to the same result
force (μ' x) = μ (force x) force (μ' x) = μ (force x)
\end{minted} \end{minted}
The monad laws have already been proven in~\cite{quotienting} and in our own formalization, we will not reiterate the proofs here. The monad laws have already been proven in~\cite{quotienting} and in our own formalization so we will not reiterate the proofs here.
\end{proof} \end{proof}
\section{An instance of K} \begin{theorem}
\todo[inline]{proof: delay is free elgot} $(Delay\;A , \approx)$ is an instance of $\mathbf{K}$ in the category $\setoids$.
\end{theorem}
\begin{proof}
We need to show that for every setoid $(A, =^A)$ the resulting setoid $(Delay\;A, \approx)$ can be extended to a stable free Elgot algebra.
Stability follows automatically by theorem~\ref{thm:stability} and the fact that $\setoids$ is cartesian closed, so it suffices to define a free elgot Algebra on $(Delay\;A, \approx)$.
Let $(X , =^X) \in \obj{\setoids}$ and $f : X \rightarrow Delay\; A + X$ be a setoid morphism, we define $f^\# : X \rightarrow Delay\;A$ pointwise:
\[
f^\# (x) :=
\begin{cases}
a & \text{if } f\;x = i_1 (a)\\
later\;(f^{\#'} a) & \text{if } f\;x = i_2 (a)
\end{cases}
\]
where $f^{\#'} : X \rightarrow Delay'\;A$ is defined corecursively by:
\[
force (f^{\#'}(x)) = f^\#(x)
\]
Let us first show that $f^\#$ is a setoid morphism, i.e. given $x, y : X$ with $x =^X y$, we need to show that $f^\#(x) = f^\#(y)$. Since $f$ is a setoid morphism we know that $f(x) =^+ f(y)$ in the coproduct setoid $(Delay\;A + X, =^+)$. We proceed by case distinction on $f(x)$:
\begin{itemize}
\item Case $f(x) = i_1 (a)$:
\[f^\# (x) = a = f^\#(y)\]
\item Case $f(x) = i_2 (a)$:
\[f^\# (x) = later (f^{\#'}(a)) = f^\# (y)\]
\end{itemize}
Now we check the iteration laws:
\change[inline]{change the equivalence sign of coproducts}
\begin{itemize}
\item \textbf{Fixpoint}: We need to show that $f^\# (x) \approx ([ id , f^\# ] \circ f)(x)$:
\begin{itemize}
\item Case $f(x) =^+ i_1 (a)$:
\[ f^\#(x) \approx a \approx [ id , f^\# ] (i_1 (a)) = ([ id , f^\# ] \circ f) (x) \]
\item Case $f(x) =^+ i_2 (a)$:
\[ f^\#(x) \approx later (f^{\#'}(a)) \overset{(*)}{\approx} f^\#(a) \approx [ id , f^\# ] (i_2 (a)) \approx ([ id , f^\# ] \circ f) (x)\]
\end{itemize}
where $(*)$ follows from a general fact: any $z : Delay'\;A$ satisfies $force\;z \approx later\;z$.
\item \textbf{Uniformity}: Let $(Y , =^Y) \in \setoids$ and $g : Y \rightarrow Delay\; A + Y, h : X \rightarrow Y$ be setoid morphisms with $(id + h) \circ f = g \circ h$.
\item \textbf{Folding}:
\end{itemize}
\end{proof}