@ -20,6 +20,8 @@ import Categories.Morphism.Properties as MP
```
-->
# Exponentials of Elgot Algebras
```agda
module Category.Construction.ElgotAlgebras.Exponentials {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) (exp : ∀ {A B} → Exponential C A B) where
@ -16,23 +16,12 @@ open import Category.Ambient using (Ambient)
open import Data.Product using (∃-syntax; _,_; Σ-syntax)
```
-->
# The Delay Monad
```agda
module Monad.Instance.Delay {o ℓ e} (ambient : Ambient o ℓ e) where
open Ambient ambient
```
## Definition
The delay monad is usually defined as a coinductive type with two constructors `now : X → D X` and `later : D X → D X`, e.g. in the [agda-stdlib](https://agda.github.io/agda-stdlib/Effect.Monad.Partiality.html#1523)
We will now define it categorically by existence of final coalgebras for the functor `(X + -)` where `X` is some object.
This functor trivially sends objects `Y` to `X + Y` and functions `f` to `id + f`.
In this definition `D X` is the underlying object of the final coalgebra given by `X`.
We then use Lambek's Lemma to gain an isomorphism `D X ≅ X + D X`, whose inverse can be factored into the constructors `now` and `later`.
<!--
```agda
open M C
open MR C
open Equiv
@ -41,7 +30,14 @@ We then use Lambek's Lemma to gain an isomorphism `D X ≅ X + D X`, whose inver
open F-Coalgebra-Morphism renaming (f to u)
open F-Coalgebra
```
-->
The delay monad is usually defined as a coinductive type with two constructors `now : X → D X` and `later : D X → D X`, e.g. in the [agda-stdlib](https://agda.github.io/agda-stdlib/Effect.Monad.Partiality.html#1523)
We will now define it categorically by existence of final coalgebras for the functor `(X + -)` where `X` is some object.
This functor trivially sends objects `Y` to `X + Y` and functions `f` to `id + f`.
In this definition `D X` is the underlying object of the final coalgebra given by `X`.
We then use Lambek's Lemma to gain an isomorphism `D X ≅ X + D X`, whose inverse can be factored into the constructors `now` and `later`.
```agda
record DelayM : Set (o ⊔ ℓ ⊔ e) where
@ -78,8 +74,6 @@ We then use Lambek's Lemma to gain an isomorphism `D X ≅ X + D X`, whose inver
D₀ X = DX {X}
```
## Delay is a monad
The next step is showing that this actually yields a monad. Some parts for this are already given, we can construct `D X` from `X` and `now : D X ⇒ D X` is the monad unit.
What's missing is Kleisli-lifting, given a morphism `f : X ⇒ D Y` we need to construct a morphism `extend f : D X ⇒ D Y`.
To do so we go from `D X` to `D X + D Y` via injection and then construct a coalgebra `D X + D Y ⇒ Y + (D X + D Y)`, the final coalgebra `D Y ⇒ Y + D Y` then yields a coalgebra-morphism from `D X + D Y` to `D Y`, see the following diagram:
open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_]; _≲_ to [_][_≲_]; _≲′_ to [_][_≲′_])
private <_> = _⟨$⟩_
open _⟶_ using (cong)
open _⟶_ using (cong) renaming (to to <_>)
-- pointwise equality between setoid morphisms:
_≐_ : ∀ {c' ℓ'} {A B : Setoid c' ℓ'} → A ⟶ B → A ⟶ B → Set (c' ⊔ ℓ')
_≐_ {c'} {ℓ'} {A} {B} f g = Setoid._≈_ (A ⇨ B) f g
@ -19,20 +19,17 @@ open import Data.Product.Relation.Binary.Pointwise.NonDependent
open import Data.Product
open import Category.Ambient using (Ambient)
open import Categories.Category.CartesianClosed
open import Categories.Monad
open import Categories.Category.Instance.Setoids
open import Categories.Category.Instance.Properties.Setoids.CCC using (Setoids-CCC)
```
-->
# The delay monad on the category of setoids is an instance of K
TODO use new names defined in Delay.algda.md open the monad modules i.e.
open Monad delayMonad∼ renaming (...)
open Monad delayMonad≈ renaming (...)
# The Delay Monad Quotiented by Weak Bisimilarity is an Instance of K on the Category of Setoids
```agda
module Monad.Instance.Setoids.K {ℓ : Level} where
open _⟶_ using (cong)
open _⟶_ using (cong) renaming (to to <_>)
open import Category.Ambient.Setoids
open Ambient (setoidAmbient {ℓ} {ℓ}) using (cocartesian; distributive)
open import Monad.Instance.Setoids.Delay {ℓ} {ℓ}
@ -48,357 +45,366 @@ module Monad.Instance.Setoids.K {ℓ : Level} where
open nat
open Setoid using () renaming (Carrier to ∣_∣; _≈_ to [_][_≡_])
open eq using () renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
open DelayMonad
open DelayMonad∼
open DelayMonad≈
open Monad delayMonad∼ using () renaming (F to Delay∼; η to η∼; μ to μ∼; assoc to assoc∼; sym-assoc to sym-assoc∼; identityˡ to identityˡ∼; identityʳ to identityʳ∼)
open Monad delayMonad≈ using () renaming (F to Delay≈; η to η≈; μ to μ≈; assoc to assoc≈; sym-assoc to sym-assoc≈; identityˡ to identityˡ≈; identityʳ to identityʳ≈)
```
≡→≡ : ∀ {A : Setoid ℓℓ} {x y : ∣ A ∣} → x ≡ y → [ A ][ x ≡ y ]
≡→≡ {A} {x} {y} eq rewrite eq = ≡-refl A
Let us first show that every Delay≈ X admits an Elgot algebra structure.
iter : ∀ {A X : Setoid ℓℓ} → (∣ X ∣ → (Delay ∣ A ∣ ⊎ ∣ X ∣)) → ∣ X ∣ → Delay ∣ A ∣
iter′ : ∀ {A X : Setoid ℓℓ} → (∣ X ∣ → (Delay ∣ A ∣ ⊎ ∣ X ∣)) → ∣ X ∣ → Delay′∣ A ∣
force (iter′ {A} {X} f x) = iter {A} {X} f x
iter {A} {X} f x with f x
... | inj₁ a = a
... | inj₂ b = later (iter′ {A} {X} f b)
We start by defining the iteration operator:
conflict : ∀ {ℓ''} (X Y : Setoid ℓℓ) {Z : Set ℓ''}
{x : ∣ X ∣} {y : ∣ Y ∣} → [ X ⊎ₛ Y ][ inj₁ x ≡ inj₂ y ] → Z
conflict X Y ()
```agda
private
iter : ∀ {A X : Setoid ℓℓ} → (∣ X ∣ → (Delay ∣ A ∣ ⊎ ∣ X ∣)) → ∣ X ∣ → Delay ∣ A ∣
iter {A} {X} f x with f x
... | inj₁ a = a
... | inj₂ b = later λ { .force → iter {A} {X} f 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 ]
conflict : ∀ {ℓ''} (X Y : Setoid ℓℓ) {Z : Set ℓ''}
{x : ∣ X ∣} {y : ∣ Y ∣} → [ X ⊎ₛ Y ][ inj₁ x ≡ inj₂ y ] → Z
conflict X Y ()
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 : 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 : 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 ]
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
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
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
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))
Now we show that `iter` defines an Elgot algebra structure on `Delay≈`
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
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 is a congruence wrt to strong bisimilarity
iter∼ : ∀ {A X : Setoid ℓℓ} → (X ⟶ (Delay∼.₀ A ⊎ₛ X)) → X ⟶ Delay∼.₀ A
<iter∼{A}{X}f> = iter {A} {X} <f>
cong (iter∼ {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∼ λ { .force∼ → cong (iter∼ {A} {X} f) (inj₂-helper f x≡y eqx eqy) }
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 is a congruence wrt to weak bisimilarity
iter≈ : ∀ {A X : Setoid ℓℓ} → (X ⟶ (Delay≈.₀ A ⊎ₛ X)) → X ⟶ Delay≈.₀ A
<iter≈{A}{X}f> = iter {A} {X} <f>
cong (iter≈ {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≈ λ { .force≈ → cong (iter≈ {A} {X} f) (inj₂-helper f x≡y eqx eqy) }
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 satisfies the fixpoint law
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
... | inj₁ a = ≈-refl A
... | inj₂ a = ≈-trans A (≈-sym A later-self) (≈-refl A)
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
... | inj₁ a = ≈-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 ]
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
... | inj₁ a | inj₁ b = drop-inj₁ helper
where
helper : [ Delay≈ A ⊎ₛ X ][ inj₁ a ≡ inj₁ b ]
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
where
helper : [ Delay≈ A ⊎ₛ X ][ inj₁ a ≡ inj₂ b ]
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)
where
helper : [ Delay≈ A ⊎ₛ X ][ inj₂ a ≡ inj₁ b ]
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))
where
helper : [ Delay≈ A ⊎ₛ X ][ inj₂ a ≡ inj₂ b ]
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}
→ ([ 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 ]
iter-uni′ : ∀ {A X Y : Setoid ℓℓ} {f : X ⟶ (Delay≈ A ⊎ₛ X)} {g : Y ⟶ (Delay≈ A ⊎ₛ Y)} {h : X ⟶ Y}
→ ([ 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 ]
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}
... | inj₁ a | inj₁ b | inj₁ c | inj₁ a≈c = ≈-trans A a≈c (inj₁-helper g (≡-sym Y x≡y) eqy eqz)
... | inj₁ a | inj₁ b | inj₂ c | inj₁ _ = absurd-helper g (≡-sym Y x≡y) eqy eqz
... | inj₂ a | inj₂ b | inj₁ c | inj₂ _ = absurd-helper g x≡y eqz eqy
... | inj₂ a | inj₂ b | inj₂ c | inj₂ req = later≈ (iter-uni′ {f = f} {g = g}{h = h} eq c≡h$a)
where
-- iter satisfies the uniformity law
iter-uni : ∀ {A X Y : Setoid ℓℓ} {f : X ⟶ (Delay≈.₀ A ⊎ₛ X)} {g : Y ⟶ (Delay≈.₀ A ⊎ₛ Y)} {h : X ⟶ Y}
→ ([ 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 ]
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}
... | inj₁ a | inj₁ b | inj₁ c | inj₁ a≈c = ≈-trans A a≈c (inj₁-helper g (≡-sym Y x≡y) eqy eqz)
... | inj₁ a | inj₁ b | inj₂ c | inj₁ _ = absurd-helper g (≡-sym Y x≡y) eqy eqz
... | inj₂ a | inj₂ b | inj₁ c | inj₂ _ = absurd-helper g x≡y eqz eqy
... | inj₂ a | inj₂ b | inj₂ c | inj₂ req = later≈ λ { .force≈ → iter-uni {A} {X} {Y} {f} {g} {h} eq c≡h$a }
where
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)
where
≡→≡ : ∀ {A : Setoid ℓℓ} {x y : ∣ A ∣} → x ≡ y → [ A ][ x ≡ y ]
≡→≡ {A} {x} {y} eq rewrite eq = ≡-refl A
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 ]
(≡-sym ⟦ B ⟧ (helper#≈-cong' {z₂})) (≡-trans ⟦ B ⟧ (helper#∼-cong (∼-trans A (delta-prop₁ (≈→≲ (≈-sym A x≈y))) (∼-sym A (∼-trans A (delta-prop₁ (≈→≲ x≈y)) (race-sym≈ x≈y))))) (helper#≈-cong' {z₁})))
(helper#∼-cong (delta-prop₂ {A} ineq₁)))
-- iter respects pointwise equality
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} f g f≐g {x} {y} x≡y with <f> x in eqa | <g> y in eqb
... | inj₁ a | inj₁ b = drop-inj₁ helper
where
helper : [ Delay≈.₀ A ⊎ₛ X ][ inj₁ a ≡ inj₁ b ]
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
where
helper : [ Delay≈.₀ A ⊎ₛ X ][ inj₁ a ≡ inj₂ b ]
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)
where
helper : [ Delay≈.₀ A ⊎ₛ X ][ inj₂ a ≡ inj₁ b ]
helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delay≈.₀ A ⊎ₛ X) (cong f x≡y) f≐g
... | inj₂ a | inj₂ b = later≈ λ { .force≈ → iter≈-resp-≐ f g f≐g (drop-inj₂ helper) }
where
helper : [ Delay≈.₀ A ⊎ₛ X ][ inj₂ a ≡ inj₂ b ]
helper rewrite (≣-sym eqb) | (≣-sym eqa) = ≡-trans (Delay≈.₀ A ⊎ₛ X) (cong f x≡y) f≐g
-- Delay≈ together with iter yield an Elgot algebra
helper₁-cong''' : {x y : Delay (∣ A ∣×ℕ {ℓ})} → (x∼y : [ A ×ₛ ℕ-setoid ][ x ∼ y ]) → [ ⟦ B ⟧ ⊎ₛ (Delay∼ (A ×ₛ ℕ-setoid) ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid)) ][ helper₁''' x ≡ helper₁''' y ]
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 }
-- interesting note:
-- the following definition prevents more general universe levels, i.e. we would like to parametrize this module by two levels c and ℓ, one for carriers and one for proofs.
-- but adopting this approach would force us to talk about setoids of type Setoid ℓ (c ⊔ ℓ), this does not work with the definition below,
-- since propositional equality lives on the same level as values, this means the type below would have to look like:
-- ‖_‖ : Setoid c (c ⊔ ℓ) → Setoid c c
-- this in turn does not play together nicely with later definition.
-- discretize a setoid
‖_‖ : Setoid ℓℓ → Setoid ℓℓ
∣_∣ ‖ X ‖ = ∣ X ∣
[_][_≡_] ‖ X ‖ = _≡_
Setoid.isEquivalence ‖ X ‖ = Eq.isEquivalence
‖‖-quote : ∀ {X : Setoid ℓℓ} → ‖ X ‖ ⟶ X
_⟶_.to ‖‖-quote x = x
cong (‖‖-quote {X}) ≣-refl = ≡-refl X
disc-dom : ∀ {X : Setoid ℓℓ} → X ⟶ (Delay≈ A ⊎ₛ X) → ‖ X ‖ ⟶ (Delay∼ A ⊎ₛ ‖ X ‖)
_⟶_.to (disc-dom f) x = f ⟨$⟩ 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 ]
force∼ (iter-g-var′ {X} g {x}) = iter-g-var {X} g {x}
iter-g-var {X} g {x} with g ⟨$⟩ x
... | inj₁ a = ∼-refl 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 ]
eq₂ = Elgot-Algebra.#-Uniformity B {Delay∼.₀ (A ×ₛ ℕ-setoid {ℓ})} {Delay∼.₀ A} {helper'} {helper} {μ∼.η A ∘ Delay∼.₁ ι∼} (λ {x} → eq {x} {x} (∼-refl (A ×ₛ ℕ-setoid)))
```
To show preservation we need some facts about discretizing setoids:
```agda
-- interesting note:
-- the following definition prevents more general universe levels, i.e. we would like to parametrize this module by two levels c and ℓ, one for carriers and one for proofs.
-- but adopting this approach would force us to talk about setoids of type Setoid ℓ (c ⊔ ℓ), this does not work with the definition below,
-- since propositional equality lives on the same level as values, this means the type below would have to look like:
-- ‖_‖ : Setoid c (c ⊔ ℓ) → Setoid c c
-- this in turn does not play together nicely with later definition.
-- discretize a setoid
‖_‖ : Setoid ℓℓ → Setoid ℓℓ
∣_∣ ‖ X ‖ = ∣ X ∣
[_][_≡_] ‖ X ‖ = _≡_
Setoid.isEquivalence ‖ X ‖ = Eq.isEquivalence
‖‖-quote : ∀ {X : Setoid ℓℓ} → ‖ X ‖ ⟶ X
_⟶_.to ‖‖-quote x = x
cong (‖‖-quote {X}) ≣-refl = ≡-refl X
disc-dom : ∀ {X : Setoid ℓℓ} → X ⟶ (Delay≈.₀ A ⊎ₛ X) → ‖ X ‖ ⟶ (Delay∼.₀ A ⊎ₛ ‖ X ‖)
_⟶_.to (disc-dom f) x = f ⟨$⟩ 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 ]
force∼ (iter-g-var′ {X} g {x}) = iter-g-var {X} g {x}
iter-g-var {X} g {x} with g ⟨$⟩ x
... | inj₁ a = ∼-refl A
... | inj₂ a = later∼ (iter-g-var′ {X} g {a})
```
Now we show that helper # is iteration preserving:
```agda
preserves' : ∀ {X : Setoid ℓℓ} {g : X ⟶ (Delay≈.₀ A ⊎ₛ X)} → ∀ {x} → [ ⟦ B ⟧ ][ (delay-lift≈ ∘ (iter≈ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift≈ , inj₂ₛ ]ₛ ∘ g) # ⟨$⟩ x ]
