module Monad.Instance.Setoids.K {ℓ : Level} where
open _⟶_ using (cong) renaming (to to <_>)
open import Category.Ambient.Setoids
open Ambient (setoidAmbient {ℓ} {ℓ}) using (cocartesian; distributive)
open import Monad.Instance.Setoids.Delay {ℓ} {ℓ}
open import Monad.Instance.K (setoidAmbient {ℓ} {ℓ})
open import Algebra.Elgot cocartesian
open import Algebra.Elgot.Free cocartesian
open import Algebra.Elgot.Stable distributive
open import Category.Construction.ElgotAlgebras {C = Setoids ℓ ℓ} cocartesian
open import Monad.PreElgot (setoidAmbient {ℓ} {ℓ})
open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼_ to [_][_∼_]; _∼′_ to [_][_∼′_]; _↓_ to [_][_↓_])
open DelayMonad
open extra
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ʳ≈)
Let us first show that every Delay≈ X admits an Elgot algebra structure.
We start by defining the iteration operator:
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 }
Some helper lemmas for reasoning about coproducts
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} 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 : ∣ 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 : ∣ 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
Now we show that iter defines an Elgot algebra structure
on Delay≈
-- 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 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 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 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)
where
≡→≡ : ∀ {A : Setoid ℓ ℓ} {x y : ∣ A ∣} → x ≡ y → [ A ][ x ≡ y ]
≡→≡ {A} {x} {y} eq rewrite eq = ≡-refl A
-- iter satisfies the folding law
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} {f} {h} {inj₂ x} with h ⟨$⟩ x in eqa
... | inj₁ a = later≈ λ { .force≈ → iter-folding {A} {X} {Y} {f} {h} {inj₁ a} }
... | inj₂ a = later≈ λ { .force≈ → iter-folding {A} {X} {Y} {f} {h} {inj₂ a} }
iter-folding {A} {X} {Y} {f} {h} {inj₁ x} with f ⟨$⟩ x in eqa
... | inj₁ a = ≈-refl A
... | inj₂ a = later≈ λ { .force≈ → helper a }
where
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 A
... | inj₂ c = later≈ λ { .force≈ → helper c }
-- 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
delay-algebras-on : ∀ {A : Setoid ℓ ℓ} → Elgot-Algebra-on (Delay≈.₀ A)
delay-algebras-on {A} = record
{ _# = iter≈ {A}
; #-Fixpoint = λ {X} {f} → iter≈-fixpoint {A} {X} {f}
; #-Uniformity = λ {X} {Y} {f} {g} {h} eq {x} → iter-uni {A} {X} {Y} {f} {g} {h} eq {x} {h ⟨$⟩ x} (≡-refl Y)
; #-Folding = λ {X} {Y} {f} {h} {x} → iter-folding {A} {X} {Y} {f} {h} {x}
; #-resp-≈ = λ {X} {f} {g} f≐g {x} → iter≈-resp-≐ {A} {X} f g f≐g {x} {x} (≡-refl X)
}
delay-algebras : ∀ (A : Setoid ℓ ℓ) → Elgot-Algebra
delay-algebras A = record { A = Delay≈.₀ A ; algebra = delay-algebras-on {A}}
open Elgot-Algebra using (#-Fixpoint; #-Uniformity; #-Compositionality; #-resp-≈; #-Diamond) renaming (A to ⟦_⟧)
Next we show that these Elgot algebras are free. This suffices to show that Delay≈ is an instance of K since stability follows from the fact that Setoids is a CCC.
We first define the free object lifting:
delay-lift : ∀ {A : Setoid ℓ ℓ} {B : Elgot-Algebra} → A ⟶ ⟦ B ⟧ → Elgot-Algebra-Morphism (delay-algebras A) B
delay-lift {A} {B} f = record { h = delay-lift≈ ; preserves = λ {X} {g} {x} → preserves' {X} {g} {x} }
where
open Elgot-Algebra B using (_#)
-- Setoid-morphism wrt strong bisimilarity
helper : (Delay∼.₀ A) ⟶ (⟦ B ⟧ ⊎ₛ Delay∼.₀ A)
< helper > (now x) = inj₁ (< f > x)
< helper > (later x) = inj₂ (force x)
cong helper (now∼ x≡y) = inj₁ (cong f x≡y)
cong helper (later∼ x∼y) = inj₂ (force∼ x∼y)
helper # is the morphism we want, note that helper # is automatically a setoid morphism wrt strong bisimilarity. The tricky part is showing that helper # is a setoid morphism wrt weak bisimilarity:
-- helper # is a setoid morphism wrt weak bisimilarity
delay-lift≈ : Delay≈.₀ A ⟶ ⟦ B ⟧
< delay-lift≈ > = < helper # >
cong delay-lift≈ x≈y =
≡-trans ⟦ B ⟧
(cong (helper #) (∼-sym A (delta-prop₂ {A} ineq₂)))
(≡-trans ⟦ B ⟧
(≡-trans ⟦ B ⟧
(≡-sym ⟦ B ⟧ (helper#≈-cong' {z₂})) (≡-trans ⟦ B ⟧ (cong (helper #) (∼-trans A (delta-prop₁ (≈→≲ (≈-sym A x≈y))) (∼-sym A (∼-trans A (delta-prop₁ (≈→≲ x≈y)) (race-sym≈ x≈y))))) (helper#≈-cong' {z₁})))
(cong (helper #) (delta-prop₂ {A} ineq₁)))
where
ineq₁ = ≈→≲ {A} x≈y
ineq₂ = ≈→≲ {A} (≈-sym A x≈y)
z₁ = delta {A} ineq₁
z₂ = delta {A} ineq₂
-- key special case
-- we prove it step-wise:
-- helper # ⟨$⟩ liftF proj₁ z ≡ helper'' # ⟨$⟩ z ≡ helper' # ⟨$⟩ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z)
helper#≈-cong' : {z : Delay (∣ A ∣ × ℕ)} → [ ⟦ B ⟧ ][ helper # ⟨$⟩ liftF proj₁ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z) ]
helper#≈-cong' {z} = ≡-trans ⟦ B ⟧ (≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ eq₁) (≡-sym ⟦ B ⟧ eq₀)) eq₂
where
-- insert value on left with 0 steps
outer : A ⟶ (A ×ₛ ℕ-setoid {ℓ})
< outer > z = (z , zero)
cong outer {x} {y} x≡y = (x≡y , ≣-refl)
-- outer cancel ι
ι-cancel : (ι∼ ∘ outer) ≐ η∼.η A
ι-cancel = ∼-refl A
helper' : (Delay∼.₀ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ Delay∼.₀ (A ×ₛ ℕ-setoid))
< helper' > (now (x , zero)) = inj₁ (< f > x)
< helper' > (now (x , suc n)) = inj₂ (< Delay∼.₁ outer > (ι {A} (x , n)))
< helper' > (later y) = inj₂ (force y)
cong helper' {now (x , zero)} (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y)
cong helper' {now (x , suc n)} {now (y , suc _)} (now∼ (x≡y , ≣-refl)) = inj₂ (cong (Delay∼.₁ outer) (cong ι∼ (x≡y , ≣-refl)))
cong helper' (later∼ x∼y) = inj₂ (force∼ x∼y)
helper'' : (Delay∼.₀ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ Delay∼.₀ (A ×ₛ ℕ-setoid))
< helper'' > (now (x , _)) = inj₁ (< f > x)
< helper'' > (later y) = inj₂ (force y)
cong helper'' {now (x , _)} (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y)
cong helper'' (later∼ x∼y) = inj₂ (force∼ x∼y)
-- Follows by #-Diamond
eq₀ : ∀ {z} → [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper'' # ⟨$⟩ z ]
eq₀ {z} = ≡-trans ⟦ B ⟧
(#-resp-≈ B {Delay∼.₀ (A ×ₛ ℕ-setoid)} {helper'} step₁)
(≡-trans ⟦ B ⟧
(#-Diamond B {Delay∼.₀ (A ×ₛ ℕ-setoid)} helper''')
(#-resp-≈ B (λ {x} → (step₂ {x}))))
where
helper''' : (Delay∼.₀ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ (Delay∼.₀ (A ×ₛ ℕ-setoid) ⊎ₛ Delay∼.₀ (A ×ₛ ℕ-setoid)))
< helper''' > (now (x , zero)) = inj₁ (< f > x)
< helper''' > (now (x , suc n)) = inj₂ (inj₁ (< Delay∼.₁ outer > (ι {A} (x , n))))
< helper''' > (later y) = inj₂ (inj₂ (force y))
cong helper''' {now (x , zero)} (now∼ (x≡y , ≣-refl)) = inj₁ (cong f x≡y)
cong helper''' {now (x , suc n)} {now (y , suc _)} (now∼ (x≡y , ≣-refl)) = inj₂ (inj₁ (cong (Delay∼.₁ outer) (cong ι∼ (x≡y , ≣-refl))))
cong helper''' (later∼ x∼y) = inj₂ (inj₂ (force∼ x∼y))
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 , suc n)} = ≡-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₂ {later y} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼.₀ (A ×ₛ ℕ-setoid))
step₂ {now (a , zero)} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼.₀ (A ×ₛ ℕ-setoid))
step₂ {now (x , suc n)} = inj₁ (by-induction n)
where
by-induction : ∀ n → [ ⟦ B ⟧ ][ < ([ inj₁ₛ , inj₂ₛ ∘ [ idₛ (Delay∼.₀ (A ×ₛ ℕ-setoid)) , idₛ (Delay∼.₀ (A ×ₛ ℕ-setoid)) ]ₛ ]ₛ ∘ helper''') # > (< Delay∼.₁ outer > (ι (x , n))) ≡ f ⟨$⟩ x ]
by-induction zero = #-Fixpoint B
by-induction (suc n) = ≡-trans ⟦ B ⟧ (#-Fixpoint B) (by-induction n)
eq₁ : ∀ {z} → [ ⟦ B ⟧ ][ helper'' # ⟨$⟩ z ≡ helper # ⟨$⟩ liftF proj₁ z ]
eq₁ {z} = #-Uniformity B {f = helper''} {g = helper} {h = Delay∼.₁ proj₁ₛ} by-uni
where
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 {later x} = ≡-refl (⟦ B ⟧ ⊎ₛ Delay∼.₀ A)
eq : ∀ {x y} → [ A ×ₛ ℕ-setoid ][ x ∼ y ] → [ ⟦ B ⟧ ⊎ₛ Delay∼.₀ A ][ [ inj₁ₛ , inj₂ₛ ∘ μ∼.η A ∘ (Delay∼.₁ ι∼) ]ₛ ∘ helper' ⟨$⟩ x ≡ (helper ∘ μ∼.η A ∘ (Delay∼.₁ ι∼)) ⟨$⟩ y ]
eq (later∼ x∼y) = inj₂ (cong (μ∼.η A) (cong (Delay∼.₁ ι∼) (force∼ x∼y)))
eq {now (x , n)} {now (y , .n)} (now∼ (x∼y , ≣-refl)) = eq' {n}
where
-- helper for induction
eq' : ∀ {n} → [ ⟦ B ⟧ ⊎ₛ Delay∼.₀ A ][ [ inj₁ₛ , inj₂ₛ ∘ μ∼.η A ∘ (Delay∼.₁ ι∼) ]ₛ ∘ helper' ⟨$⟩ (now (x , n)) ≡ (helper ∘ μ∼.η A ∘ (Delay∼.₁ ι∼)) ⟨$⟩ (now (y , n)) ]
eq' {zero} = inj₁ (cong f x∼y)
eq' {suc n} = inj₂ (∼-trans A (cong (μ∼.η A) (∼-sym (Delay∼.₀ A) (Delay∼.homomorphism {f = outer} {g = ι∼} {ι (x , n)}))) (∼-trans A identityˡ∼ (cong ι∼ (x∼y , ≣-refl))))
eq₂ : [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper # ⟨$⟩ μ {A} (liftF (ι {A}) z) ]
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:
-- 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} g {x} with g ⟨$⟩ x
... | inj₁ a = ∼-refl A
... | inj₂ a = later∼ λ { .force∼ → iter-g-var {X} g {a} }
Now we show that helper # is iteration preserving:
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₂
where
step₁ : [ ⟦ B ⟧ ][ (delay-lift≈ ∘ (iter≈ {A} {X} g)) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g)) # ⟨$⟩ x ]
step₁ = ≡-trans ⟦ B ⟧ (≡-trans ⟦ B ⟧ (cong (helper #) (iter-g-var g)) (sub-step₁ (disc-dom g) {inj₂ x})) (≡-sym ⟦ B ⟧ (#-Compositionality B {f = helper} {h = disc-dom g}))
where
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 ]
sub-step₁ g {u} = ≡-sym ⟦ B ⟧ (#-Uniformity B {h = [ idₛ (Delay∼.₀ A) , iter∼ g ]ₛ} (λ {y} → last-step {y}))
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 {inj₁ (now a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼.₀ A))
last-step {inj₁ (later a)} = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼.₀ A))
last-step {inj₂ a} with g ⟨$⟩ a in eqb
... | inj₁ (now b) = ≡-refl (⟦ B ⟧ ⊎ₛ (Delay∼.₀ A))
... | inj₁ (later 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₂ = #-Uniformity B {h = ‖‖-quote} sub-step₂
where
sub-step₂ : ∀ {x} → [ ⟦ B ⟧ ⊎ₛ X ][([ inj₁ₛ , inj₂ₛ ]ₛ ∘ ([ inj₁ₛ ∘ (helper #) , inj₂ₛ ]ₛ ∘ (disc-dom g))) ⟨$⟩ x ≡ ([ inj₁ₛ ∘ delay-lift≈ , inj₂ₛ ]ₛ ∘ g) ⟨$⟩ x ]
sub-step₂ {x} with g ⟨$⟩ x
... | inj₁ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
... | inj₂ y = ≡-refl (⟦ B ⟧ ⊎ₛ X)
open Elgot-Algebra-Morphism using (preserves) renaming (h to <<_>>)
Only uniqueness of delaylift is left now:
freeAlgebra : ∀ (A : Setoid ℓ ℓ) → FreeObject elgotForgetfulF A
freeAlgebra A = record
{ FX = delay-algebras A
; η = η≈.η A
; _* = delay-lift
; *-lift = λ {B} f {x} → Elgot-Algebra.#-Fixpoint B
; *-uniq = λ {B} f g eq {x} → *-uniq' {B} f g (delay-lift f) eq (#-Fixpoint B) {x}
}
where
*-uniq' : ∀ {B : Elgot-Algebra} (f : A ⟶ ⟦ B ⟧) (g h : Elgot-Algebra-Morphism (delay-algebras A) B)
→ (<< g >> ∘ (η≈.η A)) ≐ f
→ (<< h >> ∘ (η≈.η A)) ≐ f
→ << g >> ≐ << h >>
*-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 ⟧ (#-resp-≈ B (λ {x} → helper-eq' {x}) {x})
(≡-trans ⟦ B ⟧ (≡-sym ⟦ B ⟧ (preserves h {Delay∼.₀ A} {[ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now} {x = x}))
(≡-sym ⟦ B ⟧ (cong << h >> iter-id)))))
where
open Elgot-Algebra B using (_#)
D∼⇒D≈ : ∀ {A : Setoid ℓ ℓ} → Delay∼.₀ A ⟶ Delay≈.₀ A
D∼⇒D≈ {A} = record { to = λ x → x ; cong = λ eq → ∼⇒≈ eq }
-- setoid morphism that unfolds a computation (works like 'out') but lifts the value to a computation
-- the point of this definition is that 'helper-now # = id'
helper-now : Delay∼.₀ A ⟶ ((Delay∼.₀ A) ⊎ₛ (Delay∼.₀ A))
< helper-now > (now x) = inj₁ (now x)
< helper-now > (later x) = inj₂ (force x)
cong helper-now (now∼ eq) = inj₁ (now∼ eq)
cong helper-now (later∼ eq) = inj₂ (force∼ eq)
iter-id : ∀ {x} → [ A ][ x ≈ iter≈ ([ inj₁ₛ ∘ D∼⇒D≈ , inj₂ₛ ]ₛ ∘ helper-now) ⟨$⟩ x ]
iter-id {now x} = ≈-refl A
iter-id {later x} = later≈ λ { .force≈ → iter-id }
-- the 'meat' of this proof:
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 ]
helper-eq' {now x} = inj₁ (≡-trans ⟦ B ⟧ eqᵍ (≡-sym ⟦ B ⟧ eqʰ))
helper-eq' {later x} = inj₂ (∼-refl A)
-- stability follows automatically since Setoids is cartesian closed
open CartesianClosed (Setoids-CCC ℓ) renaming (exp to setoid-exp)
open import Algebra.Elgot.Properties distributive setoid-exp using (free-isStable)
delayK : MonadK
delayK = record { freealgebras = freeAlgebra ; stable = λ X → free-isStable (freeAlgebra X) }