diff --git a/agda/src/Monad/Instance/Setoids/Delay.lagda.md b/agda/src/Monad/Instance/Setoids/Delay.lagda.md index 6ccfc54..95f81a5 100644 --- a/agda/src/Monad/Instance/Setoids/Delay.lagda.md +++ b/agda/src/Monad/Instance/Setoids/Delay.lagda.md @@ -176,10 +176,10 @@ open Bisimilarity renaming (_≈_ to [_][_≈_]; _≈′_ to [_][_≈′_]; _∼ module DelayMonad where - 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ₛ∼ : 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≈ : 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∼ : Setoid c (c ⊔ ℓ) → Setoid c (c ⊔ ℓ) + Delay∼ A = record { Carrier = Delay ∣ A ∣ ; _≈_ = [_][_∼_] A ; isEquivalence = record { refl = ∼-refl A ; sym = ∼-sym A ; trans = ∼-trans A } } <_> = _⟨$⟩_ 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) 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 : 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 } where ∼-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} {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} {now x} = ≈-refl A 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) 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 } η-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} (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} {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 μ↓ {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} {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} {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} {later y} (↓≈ a≡b (later↓ x↓a) (later↓ y↓b)) = later≈ (μ-cong′ A (≈→≈′ (Delayₛ A) (↓≈ a≡b x↓a y↓b))) + μ-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} {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) 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 : Setoid c (c ⊔ ℓ)) → Delayₛ∼ (Delayₛ∼ A) ⟶ Delayₛ∼ A + μₛ∼ : ∀ (A : Setoid c (c ⊔ ℓ)) → Delay∼ (Delay∼ A) ⟶ Delay∼ A μₛ∼ A = record { to = μ {A} ; cong = μ-cong∼ A } 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) μ-cong∼ A {.(now _)} {.(now _)} (now∼ x∼y) = 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 {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} μ-assoc' {A} {now x} = ∼-refl A μ-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}) 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ˡ∼′ 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 ] force≈ (identityˡ′ {A} {x}) = identityˡ identityˡ {A} {now x} = ≈-refl A 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} {later x} = ≈-refl A delayMonad : Monad (Setoids c (c ⊔ ℓ)) delayMonad = record { F = record - { F₀ = Delayₛ + { F₀ = Delay≈ ; F₁ = liftFₛ ; identity = lift-id ; 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 , suc n) = later (ι′ (x , n)) - ιₛ' : (A ×ₛ (ℕ-setoid {c})) ⟶ Delayₛ∼ A + ιₛ' : (A ×ₛ (ℕ-setoid {c})) ⟶ Delay∼ A ιₛ' = record { to = ι ; cong = ι-cong } where ι-cong : ∀ {x y} → [ A ×ₛ (ℕ-setoid {c}) ][ x ≡ y ] → [ A ][ ι x ∼ ι y ] diff --git a/agda/src/Monad/Instance/Setoids/K.lagda.md b/agda/src/Monad/Instance/Setoids/K.lagda.md index 46dc08f..a461c5b 100644 --- a/agda/src/Monad/Instance/Setoids/K.lagda.md +++ b/agda/src/Monad/Instance/Setoids/K.lagda.md @@ -76,8 +76,8 @@ module Monad.Instance.Setoids.K {ℓ : Level} 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 ⟶ (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 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 @@ -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 = 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 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 @@ -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 = 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 : 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-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 ... | 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 ] + 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 + 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) + 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 + 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 + 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₁ₛ ∘ (idₛ (Delayₛ A)) , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) + 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₁ₛ ∘ (idₛ (Delayₛ A)) , inj₂ₛ ∘ h ]ₛ ∘ f) ≋ (g ∘ h) + 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 ] 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} @@ -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) 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) - 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} iter-folding {A} {X} {Y} {f} {h} {inj₁ x} with f ⟨$⟩ x in eqa ... | 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}) - 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 { _# = iterₛ {A} ; #-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 = 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 ⟦_⟧) @@ -183,12 +183,12 @@ module Monad.Instance.Setoids.K {ℓ : Level} where helper₁ (now x) = inj₁ (< f > 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 (later∼ x≡y) = inj₂ (force∼ x≡y) -- -- 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#∼-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₁' (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 , 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' : (Delayₛ∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ Delayₛ∼ (A ×ₛ ℕ-setoid)) + helper' : (Delay∼ (A ×ₛ ℕ-setoid)) ⟶ (⟦ B ⟧ ⊎ₛ Delay∼ (A ×ₛ ℕ-setoid)) helper' = record { to = helper₁' ; cong = helper₁-cong'} helper₁'' : Delay (∣ A ∣ × ℕ {ℓ}) → ∣ ⟦ B ⟧ ∣ ⊎ Delay (∣ A ∣ × ℕ {ℓ}) helper₁'' (now (x , _)) = inj₁ (< f > x) 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'' (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''} -- Needs #-Diamond eq₀ : ∀ {z} → [ ⟦ B ⟧ ][ helper' # ⟨$⟩ z ≡ helper'' # ⟨$⟩ z ] eq₀ {z} = ≡-trans ⟦ B ⟧ - (#-resp-≈ B {Delayₛ∼ (A ×ₛ ℕ-setoid)} {helper'} step₁) + (#-resp-≈ B {Delay∼ (A ×ₛ ℕ-setoid)} {helper'} step₁) (≡-trans ⟦ B ⟧ - (#-Diamond B {Delayₛ∼ (A ×ₛ ℕ-setoid)} helper''') + (#-Diamond B {Delay∼ (A ×ₛ ℕ-setoid)} helper''') (#-resp-≈ B (λ {x} → (step₂ {x})))) where 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₁''' (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 , 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''' : (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''' } - 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) ][ 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₂ {now (a , zero)} = ≡-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₂ {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''') # > (< 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 (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} = #-Uniformity B {f = helper''} {g = helper} {h = liftFₛ∼ 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) + 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₂ ∘′ μ ∘′ (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} 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' {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₂ : [ ⟦ 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 } @@ -307,34 +307,34 @@ module Monad.Instance.Setoids.K {ℓ : Level} where _⟶_.to ‖‖-quote x = 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 - 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} 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 ] + 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 ⟧ (helper#∼-cong (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 + 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})) + 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 : ∀ {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)) + ... | 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 @@ -359,23 +359,23 @@ module Monad.Instance.Setoids.K {ℓ : Level} where → (<< 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 ⟧ (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})) + (≡-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 : Setoid ℓ ℓ} → Delay∼ A ⟶ Delay≈ A D∼⇒D≈ {A} = record { to = λ x → x ; cong = λ eq → ∼⇒≈ eq } helper-now₁ : (Delay ∣ A ∣) → (Delay ∣ A ∣ ⊎ (Delay ∣ A ∣)) helper-now₁ (now x) = inj₁ (now 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) ; (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 ] helper-eq' {now x} = inj₁ (≡-trans ⟦ B ⟧ eqᵍ (≡-sym ⟦ B ⟧ eqʰ)) helper-eq' {later x} = inj₂ (∼-refl A) diff --git a/thesis/src/04_iteration.tex b/thesis/src/04_iteration.tex index f4af006..3992d3c 100644 --- a/thesis/src/04_iteration.tex +++ b/thesis/src/04_iteration.tex @@ -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: -\begin{theorem} +\begin{theorem}\label{thm:stability} In a cartesian closed category every free Elgot algebra is stable. \end{theorem} \begin{proof} diff --git a/thesis/src/05_setoids.tex b/thesis/src/05_setoids.tex index 133ac5b..4524a96 100644 --- a/thesis/src/05_setoids.tex +++ b/thesis/src/05_setoids.tex @@ -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$. \improvement[inline]{Text is not good} +\todo[inline]{sketch the proof that setoids is CCC and cocartesian} \section{Quotienting the Delay Monad} @@ -34,7 +35,7 @@ codata (A : Set) : Set where later : Delay A → Delay A \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} @@ -70,7 +71,7 @@ We will now introduce two notions of equality on inhabitants of the delay type, $(Delay\;A, \sim)$ is a setoid. \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 @@ -102,9 +103,57 @@ Now we can relate two computations \textit{iff} they evaluate to the same result force (μ' x) = μ (force x) \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} -\section{An instance of K} -\todo[inline]{proof: delay is free elgot} +\begin{theorem} + $(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}