diff --git a/agda/Makefile b/agda/Makefile
index ba3f8f4..1c5489b 100644
--- a/agda/Makefile
+++ b/agda/Makefile
@@ -29,7 +29,6 @@ push: all
Everything.agda:
echo "{-# OPTIONS --guardedness #-}" > src/Everything.agda
git ls-files | egrep '^src/[^\.]*.l?agda(\.md)?' | grep -v 'index.lagda.md' | grep -v 'bsc.agda-lib' | sed -e 's|^src/[/]*|import |' -e 's|/|.|g' -e 's/.agda//' -e '/import Everything/d' -e 's/..md//' | LC_COLLATE='C' sort >> src/Everything.agda
-
open:
firefox public/index.html
diff --git a/agda/src/Category/Ambient.lagda.md b/agda/src/Category/Ambient.lagda.md
index bf66540..3462e58 100644
--- a/agda/src/Category/Ambient.lagda.md
+++ b/agda/src/Category/Ambient.lagda.md
@@ -29,28 +29,22 @@ import Categories.Morphism.Properties as MP'
-->
## Summary
-We work in an ambient category that
-
-- is extensive (has finite coproducts and pullbacks along injections)
-- is cartesian (has finite products, extensive + cartesian also gives a distributivity isomorphism)
-- has a parametrized NNO ℕ
-- has exponentials `X^ℕ`
+We work in an ambient distributive category.
+This file contains some helper definitions that will be used throughout the development.
```agda
module Category.Ambient where
- record Ambient (o ℓ e : Level) : Set (suc o ⊔ suc ℓ ⊔ suc e) where
+ record Ambient (o ℓ e : Level) : Set (suc (o ⊔ ℓ ⊔ e)) where
field
C : Category o ℓ e
- extensive : Extensive C
- cartesian : Cartesian C
- ℕ : ParametrizedNNO (record { U = C ; cartesian = cartesian })
- -- _^ℕ : ∀ X → Exponential C (ParametrizedNNO.N ℕ) X
+ distributive : Distributive C
+
+ open Distributive distributive public
cartesianCategory : CartesianCategory o ℓ e
cartesianCategory = record { U = C ; cartesian = cartesian }
open Category C renaming (id to idC) public
- open Extensive extensive public
open Cocartesian cocartesian renaming (+-unique to []-unique) public
open Cartesian cartesian public
@@ -65,14 +59,9 @@ module Category.Ambient where
braided = Symmetric.braided symmetric
open BinaryProducts products renaming (η to ⁂-η; g-η to ⁂-g-η; unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′) public
- open ParametrizedNNO ℕ public renaming (η to pnno-η)
-
open CartesianMonoidal cartesian using (⊤×A≅A; A×⊤≅A) public
- distributive : Distributive C
- distributive = Extensive×Cartesian⇒Distributive C extensive cartesian
- open Distributive distributive hiding (cartesian; cocartesian) public
open M' C
open HomReasoning
open MR' C
diff --git a/agda/src/Category/Ambient/Setoids.lagda.md b/agda/src/Category/Ambient/Setoids.lagda.md
index 38182ba..8df6541 100644
--- a/agda/src/Category/Ambient/Setoids.lagda.md
+++ b/agda/src/Category/Ambient/Setoids.lagda.md
@@ -1,114 +1,46 @@
# The category of Setoids can be used as instance for ambient category
-Most of the required properties are already proven in the agda-categories library, we are only left to construct the natural numbers object.
+Most of the required properties are already proven in the agda-categories library, we are only left to show distributivity.
```agda
-module Category.Ambient.Setoids {ℓ} where
- open _⟶_ using (cong)
+module Category.Ambient.Setoids {c ℓ} where
+ open M (Setoids c (c ⊔ ℓ))
+ open _⟶_ using (cong) renaming (to to <_>)
- -- equality on setoid functions
- private
- _≋_ : ∀ {A B : Setoid ℓ ℓ} → A ⟶ B → A ⟶ B → Set ℓ
- _≋_ {A} {B} f g = Setoid._≈_ (A ⇨ B) f g
- ≋-sym : ∀ {A B : Setoid ℓ ℓ} {f g : A ⟶ B} → f ≋ g → g ≋ f
- ≋-sym {A} {B} {f} {g} = IsEquivalence.sym (Setoid.isEquivalence (A ⇨ B)) {f} {g}
- ≋-trans : ∀ {A B : Setoid ℓ ℓ} {f g h : A ⟶ B} → f ≋ g → g ≋ h → f ≋ h
- ≋-trans {A} {B} {f} {g} {h} = IsEquivalence.trans (Setoid.isEquivalence (A ⇨ B)) {f} {g} {h}
+ refl : ∀ (A : Setoid c (c ⊔ ℓ)) {a} → Setoid._≈_ A a a
+ refl A = IsEquivalence.refl (Setoid.isEquivalence A)
- -- we define ℕ ourselves, instead of importing it, to avoid lifting the universe levels (builtin Nats are defined on Set₀)
- data ℕ : Set ℓ where
- zero : ℕ
- suc : ℕ → ℕ
+ setoidDistributive : Distributive (Setoids c (c ⊔ ℓ))
+ Distributive.cartesian setoidDistributive = Setoids-Cartesian
+ Distributive.cocartesian setoidDistributive = Setoids-Cocartesian {c} {(c ⊔ ℓ)}
+ < IsIso.inv (Distributive.isIsoˡ setoidDistributive {A} {B} {C}) > (x , (inj₁ y)) = inj₁ (x , y)
+ < IsIso.inv (Distributive.isIsoˡ setoidDistributive {A} {B} {C}) > (x , (inj₂ y)) = inj₂ (x , y)
+ cong (IsIso.inv (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {(x , inj₁ y)} {(a , inj₁ b)} (x≈a , inj₁ y≈b) = inj₁ (x≈a , y≈b)
+ cong (IsIso.inv (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {(x , inj₂ y)} {(a , inj₂ b)} (x≈a , inj₂ y≈b) = inj₂ (x≈a , y≈b)
+ Iso.isoˡ (IsIso.iso (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {inj₁ (a , b)} = inj₁ (refl A , refl B)
+ Iso.isoˡ (IsIso.iso (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {inj₂ (a , c)} = inj₂ (refl A , refl C)
+ Iso.isoʳ (IsIso.iso (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {a , inj₁ b} = refl A , inj₁ (refl B)
+ Iso.isoʳ (IsIso.iso (Distributive.isIsoˡ setoidDistributive {A} {B} {C})) {a , inj₂ c} = (refl A) , (inj₂ (refl C))
- suc-cong : ∀ {n m} → n ≡ m → suc n ≡ suc m
- suc-cong n≡m rewrite n≡m = Eq.refl
-
- suc-inj : ∀ {n m} → suc n ≡ suc m → n ≡ m
- suc-inj Eq.refl = Eq.refl
-
- ℕ-eq : Rel ℕ ℓ
- ℕ-eq zero zero = ⊤
- ℕ-eq zero (suc m) = ⊥
- ℕ-eq (suc n) zero = ⊥
- ℕ-eq (suc n) (suc m) = ℕ-eq n m
-
- ⊤-setoid : Setoid ℓ ℓ
- ⊤-setoid = record { Carrier = ⊤ ; _≈_ = _≡_ ; isEquivalence = Eq.isEquivalence }
-
- ℕ-setoid : Setoid ℓ ℓ
- ℕ-setoid = record
- { Carrier = ℕ
- ; _≈_ = _≡_ -- ℕ-eq
- ; isEquivalence = Eq.isEquivalence
+ setoidAmbient : Ambient (ℓ-suc (c ⊔ ℓ)) (c ⊔ ℓ) (c ⊔ ℓ)
+ setoidAmbient = record
+ { C = Setoids c (c ⊔ ℓ)
+ ; distributive = setoidDistributive
}
-
- zero⟶ : SingletonSetoid {ℓ} {ℓ} ⟶ ℕ-setoid
- zero⟶ = record { to = λ _ → zero ; cong = λ x → Eq.refl }
- suc⟶ : ℕ-setoid ⟶ ℕ-setoid
- suc⟶ = record { to = suc ; cong = suc-cong }
-
- ℕ-universal : ∀ {A : Setoid ℓ ℓ} → SingletonSetoid {ℓ} {ℓ} ⟶ A → A ⟶ A → ℕ-setoid ⟶ A
- ℕ-universal {A} z s = record { to = app ; cong = cong' }
- where
- app : ℕ → Setoid.Carrier A
- app zero = z ⟨$⟩ tt
- app (suc n) = s ⟨$⟩ (app n)
- cong' : ∀ {n m : ℕ} → n ≡ m → Setoid._≈_ A (app n) (app m)
- cong' Eq.refl = IsEquivalence.refl (Setoid.isEquivalence A)
-
- ℕ-z-commute : ∀ {A : Setoid ℓ ℓ} {q : SingletonSetoid {ℓ} {ℓ} ⟶ A} {f : A ⟶ A} → q ≋ (ℕ-universal q f ∘ zero⟶)
- ℕ-z-commute {A} {q} {f} {lift t} = IsEquivalence.refl (Setoid.isEquivalence A)
-
- ℕ-s-commute : ∀ {A : Setoid ℓ ℓ} {q : SingletonSetoid {ℓ} {ℓ} ⟶ A} {f : A ⟶ A} → (f ∘ (ℕ-universal q f)) ≋ (ℕ-universal q f ∘ suc⟶)
- ℕ-s-commute {A} {q} {f} {n} = IsEquivalence.refl (Setoid.isEquivalence A)
-
- ℕ-unique : ∀ {A : Setoid ℓ ℓ} {q : SingletonSetoid {ℓ} {ℓ} ⟶ A} {f : A ⟶ A} {u : ℕ-setoid ⟶ A} → q ≋ (u ∘ zero⟶) → (f ∘ u) ≋ (u ∘ suc⟶) → u ≋ ℕ-universal q f
- ℕ-unique {A} {q} {f} {u} qz fs {zero} = ≋-sym {SingletonSetoid} {A} {q} {u ∘ zero⟶} qz
- ℕ-unique {A} {q} {f} {u} qz fs {suc n} = AR.begin
- u ⟨$⟩ suc n AR.≈⟨ ≋-sym {ℕ-setoid} {A} {f ∘ u} {u ∘ suc⟶} fs ⟩
- f ∘ u ⟨$⟩ n AR.≈⟨ cong f (ℕ-unique {A} {q} {f} {u} qz fs {n}) ⟩
- f ∘ ℕ-universal q f ⟨$⟩ n AR.≈⟨ ℕ-s-commute {A} {q} {f} {n} ⟩
- ℕ-universal q f ⟨$⟩ suc n AR.∎
- where module AR = SetoidR A
-
- setoidNNO : NNO (Setoids ℓ ℓ) SingletonSetoid-⊤
- setoidNNO = record
- { N = ℕ-setoid
- ; isNNO = record
- { z = zero⟶
- ; s = suc⟶
- ; universal = ℕ-universal
- ; z-commute = λ {A} {q} {f} → ℕ-z-commute {A} {q} {f}
- ; s-commute = λ {A} {q} {f} {n} → ℕ-s-commute {A} {q} {f} {n}
- ; unique = λ {A} {q} {f} {u} qz fs → ℕ-unique {A} {q} {f} {u} qz fs
- }
- }
-
- setoidAmbient : Ambient (ℓ-suc ℓ) ℓ ℓ
- setoidAmbient = record { C = Setoids ℓ ℓ ; extensive = Setoids-Extensive ℓ ; cartesian = Setoids-Cartesian ; ℕ = NNO×CCC⇒PNNO (record { U = Setoids ℓ ℓ ; cartesianClosed = Setoids-CCC ℓ }) (Cocartesian.coproducts (Setoids-Cocartesian {ℓ} {ℓ})) setoidNNO }
```
\ No newline at end of file
diff --git a/agda/src/Monad/Instance/Delay.lagda.md b/agda/src/Monad/Instance/Delay.lagda.md
index f7f4959..f5734a8 100644
--- a/agda/src/Monad/Instance/Delay.lagda.md
+++ b/agda/src/Monad/Instance/Delay.lagda.md
@@ -96,25 +96,6 @@ Since `Y ⇒ X + Y` is an algebra for the `(X + -)` functor, we can use the fina
(idC +₁ coit g) ∘ f ∎ })
```
-Furthermore if we combine the internal algebra structure of Parametrized NNOs with Lambek's lemma, we get the isomorphism `X × N ≅ X + X × N`.
-At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `(Y + \_)`-functor defined above, this gives us another morphism `ι : X × N ⇒ DX` by using the final coalgebras.
-
-
-
-```agda
- nno-iso : X × N ≅ X + X × N
- nno-iso = Lambek.lambek (record { ⊥ = PNNO-Algebra cartesianCategory coproducts X N z s ; ⊥-is-initial = PNNO⇒Initial₂ cartesianCategory coproducts ℕ X })
-
- ι-coalg : F-Coalgebra-Morphism (record { A = X × N ; α = _≅_.from nno-iso }) (record { A = DX ; α = out })
- ι-coalg = ! {A = record { A = X × N ; α = _≅_.from nno-iso }}
-
- ι : X × N ⇒ DX
- ι = u ι-coalg
-
- ι-commutes : out ∘ ι ≈ (idC +₁ ι) ∘ _≅_.from nno-iso
- ι-commutes = commutes ι-coalg
-```
-
## 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.
@@ -254,7 +235,7 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
[ [ (idC +₁ extend' ([ now , f ])) ∘ i₁ , (idC +₁ extend' ([ now , f ])) ∘ h ] , i₂ ∘ extend' ([ now , f ]) ] ∘ out ≈˘⟨ ([]-cong₂ ∘[] +₁∘i₂) ⟩∘⟨refl ⟩
[ (idC +₁ extend' ([ now , f ])) ∘ [ i₁ , h ] , (idC +₁ extend' ([ now , f ])) ∘ i₂ ] ∘ out ≈˘⟨ pullˡ ∘[] ⟩
(idC +₁ extend' ([ now , f ])) ∘ [ [ i₁ , h ] , i₂ ] ∘ out ∎ }))) ⟩∘⟨refl ⟩
- u (Terminal.! (coalgebras Y)) ∘ g ≈⟨ (Terminal.!-unique (coalgebras Y) (record { f = extend' ([ now , i ]) ; commutes = begin
+ u (Terminal.! (coalgebras Y)) ∘ g ≈⟨ (Terminal.!-unique (coalgebras Y) {A = record { A = A (Terminal.⊤ (coalgebras (Y + X))) ; α = [ [ i₁ , h ] , i₂ ] ∘ out }} (record { f = extend' ([ now , i ]) ; commutes = begin
out ∘ extend' ([ now , i ]) ≈⟨ extendlaw ([ now , i ]) ⟩
[ out ∘ [ now , i ] , i₂ ∘ extend' ([ now , i ]) ] ∘ out ≈⟨ ([]-cong₂ ∘[] refl) ⟩∘⟨refl ⟩
[ [ out ∘ now , out ∘ i ] , i₂ ∘ extend' ([ now , i ]) ] ∘ out ≈⟨ ([]-cong₂ ([]-cong₂ unitlaw (helper i eqi)) refl) ⟩∘⟨refl ⟩
diff --git a/agda/src/Monad/Instance/Delay/Quotienting.lagda.md b/agda/src/Monad/Instance/Delay/Quotienting.lagda.md
deleted file mode 100644
index ca8642a..0000000
--- a/agda/src/Monad/Instance/Delay/Quotienting.lagda.md
+++ /dev/null
@@ -1,159 +0,0 @@
-
-
-```agda
-module Monad.Instance.Delay.Quotienting {o ℓ e} (ambient : Ambient o ℓ e) where
- open Ambient ambient
- open import Categories.Diagram.Coequalizer C
- open import Monad.Instance.Delay ambient
- open F-Coalgebra-Morphism using () renaming (f to u; commutes to coalg-commutes)
-```
-
-
-# Quotienting the delay monad by weak bisimilarity
-
-The coinductive definition of the delay monad yields a 'wrong' kind of equality called *strong bisimilarity*, which differentiates between computations with different execution times, instead we want two computations to be equal, when they both terminate with the same result (or don't terminate at all).
-This is called *weak bisimilarity*. The ideas is then to quotient the delay monad with this 'right' kind of equality and show that the result $\tilde{D}$ is again a (strong) monad.
-
-In category theory existence of **coequalizers** corresponds to qoutienting, so we will express the quotiented delay monad via the following coequalizer:
-
-
-
-
-## Preliminaries
-
-Existence of the coequalizer doesn't suffice, we will need some conditions having to do with preservation of the coequalizer, so let's first define what it means for a coequalizer to be preserved by an endofunctor:
-
-```agda
- preserves : ∀ {X Y} {f g : X ⇒ Y} → Endofunctor C → Coequalizer f g → Set (o ⊔ ℓ ⊔ e)
- preserves {X} {Y} {f} {g} F coeq = IsCoequalizer (Functor.₁ F f) (Functor.₁ F g) (Functor.₁ F (Coequalizer.arr coeq))
-```
-
-We will now show that the following conditions are equivalent:
-
-1. For every $X$, the coequalizer is preserved by $D$
-2. every $\tilde{D}X$ extends to a search-algebra, so that each $ρ_X$ is a D-algebra morphism
-3. for every $X$, $(\tilde{D}X, ρ ∘ now : X → \tilde{D}X)$ is a stable free elgot algebra on X, $ρ_X$ is a D-algebra morphism and $ρ_X = ((ρ_X ∘ now + id) ∘ out)^\#$
-4. $\tilde{D}$ extends to a strong monad, so that $ρ$ is a strong monad morphism
-
-```agda
- module _ (D : DelayM) where
- open DelayM D renaming (functor to D-Functor; monad to D-Monad; kleisli to D-Kleisli)
-
- open Functor D-Functor using () renaming (F₁ to D₁; homomorphism to D-homomorphism; F-resp-≈ to D-resp-≈; identity to D-identity)
- open RMonad D-Kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ; identityˡ to k-identityˡ)
- open Monad D-Monad using () renaming (assoc to M-assoc; identityʳ to M-identityʳ)
- open HomReasoning
- open M C
- open MR C
- open Equiv
-
- module Quotiented (coeqs : ∀ X → Coequalizer (extend (ι {X})) (D₁ π₁)) where
-
- Ď₀ : Obj → Obj
- Ď₀ X = Coequalizer.obj (coeqs X)
-
- ρ : ∀ {X} → D₀ X ⇒ Ď₀ X
- ρ {X} = Coequalizer.arr (coeqs X)
-
- ρ-epi : ∀ {X} → Epi (ρ {X})
- ρ-epi {X} = Coequalizer⇒Epi (coeqs X)
-
- ρ▷ : ∀ {X} → ρ ∘ ▷ ≈ ρ {X}
- ρ▷ {X} = sym (begin
- ρ ≈⟨ introʳ intro-helper ⟩
- ρ ∘ D₁ π₁ ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullˡ (sym equality) ⟩
- (ρ ∘ extend ι) ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ (sym k-assoc) ⟩
- ρ ∘ extend (extend ι ∘ now ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩) ≈⟨ (refl⟩∘⟨ extend-≈ (pullˡ k-identityʳ)) ⟩
- ρ ∘ extend (ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩) ≈⟨ (refl⟩∘⟨ extend-≈ helper) ⟩
- ρ ∘ extend (▷ ∘ now) ≈⟨ (refl⟩∘⟨ sym (▷∘extendʳ now)) ⟩
- ρ ∘ extend now ∘ ▷ ≈⟨ elim-center k-identityˡ ⟩
- ρ ∘ ▷ ∎)
- where
- open Coequalizer (coeqs X) using (equality; coequalize; id-coequalize; coequalize-resp-≈) renaming (universal to coeq-universal; unique to coeq-unique; unique′ to coeq-unique′)
- intro-helper : D₁ π₁ ∘ D₁ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈ idC
- intro-helper = sym D-homomorphism ○ D-resp-≈ project₁ ○ D-identity
- helper : ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈ ▷ ∘ now
- helper = begin
- ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩
- (out⁻¹ ∘ out) ∘ ι ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ (pullˡ (coalg-commutes ((Terminal.! (coalgebras X) {A = record { A = X × N ; α = _≅_.from nno-iso }})))) ⟩
- out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ ⟨ idC , s ∘ z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identity² refl)) ⟩
- out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (idC ⁂ s) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym inject₂ ⟩∘⟨refl) ⟩
- out⁻¹ ∘ ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (_≅_.to nno-iso ∘ i₂) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ (pullʳ (pullˡ (cancelˡ (_≅_.isoʳ nno-iso))))) ⟩
- out⁻¹ ∘ (idC +₁ ι) ∘ i₂ ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ pullˡ +₁∘i₂) ⟩
- out⁻¹ ∘ (i₂ ∘ ι) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ sym inject₁) ⟩
- out⁻¹ ∘ (i₂ ∘ ι) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ intro-center (_≅_.isoˡ out-≅) ⟩∘⟨refl) ⟩
- out⁻¹ ∘ (i₂ ∘ (out⁻¹ ∘ out) ∘ ι) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ (refl⟩∘⟨ pullʳ (coalg-commutes ((Terminal.! (coalgebras X) {A = record { A = X × N ; α = _≅_.from nno-iso }})))) ⟩∘⟨refl) ⟩
- out⁻¹ ∘ (i₂ ∘ out⁻¹ ∘ (idC +₁ ι) ∘ _≅_.from nno-iso) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ (refl⟩∘⟨ (pullʳ (pullˡ (pullʳ (cancelʳ (_≅_.isoʳ nno-iso)))))) ⟩
- out⁻¹ ∘ i₂ ∘ (out⁻¹ ∘ (idC +₁ ι)) ∘ i₁ ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ pullʳ +₁∘i₁) ⟩
- out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁ ∘ idC ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ) ⟩
- out⁻¹ ∘ i₂ ∘ out⁻¹ ∘ i₁ ≈⟨ ((refl⟩∘⟨ sym-assoc) ○ assoc²'') ⟩
- ▷ ∘ now ∎
-
- Ď-Functor : Endofunctor C
- Ď-Functor = record
- { F₀ = Ď₀
- ; F₁ = F₁'
- ; identity = λ {X} → Coequalizer.coequalize-resp-≈ (coeqs X) (elimʳ D-identity) ○ sym (Coequalizer.id-coequalize (coeqs X))
- ; homomorphism = λ {X} {Y} {Z} {f} {g} → sym (Coequalizer.unique (coeqs X) (sym (begin
- (F₁' g ∘ F₁' f) ∘ ρ ≈⟨ pullʳ (sym (Coequalizer.universal (coeqs X))) ⟩
- F₁' g ∘ ρ ∘ D₁ f ≈⟨ pullˡ (sym (Coequalizer.universal (coeqs Y))) ⟩
- (ρ ∘ D₁ g) ∘ D₁ f ≈⟨ pullʳ (sym D-homomorphism) ⟩
- ρ ∘ D₁ (g ∘ f) ∎)))
- ; F-resp-≈ = λ {X} {Y} {f} {g} eq → Coequalizer.coequalize-resp-≈ (coeqs X) (refl⟩∘⟨ (D-resp-≈ eq))
- }
- where
- F₁' : ∀ {X} {Y} (f : X ⇒ Y) → Ď₀ X ⇒ Ď₀ Y
- F₁' {X} {Y} f = coequalize {h = ρ ∘ D₁ f} (begin
- (ρ ∘ D₁ f) ∘ extend ι ≈⟨ pullʳ (sym k-assoc) ⟩
- ρ ∘ extend (extend (now ∘ f) ∘ ι) ≈⟨ refl⟩∘⟨ (extend-≈ (sym (Terminal.!-unique (coalgebras Y) (record { f = extend (now ∘ f) ∘ ι ; commutes = begin
- out ∘ extend (now ∘ f) ∘ ι ≈⟨ pullˡ (extendlaw (now ∘ f)) ⟩
- ([ out ∘ now ∘ f , i₂ ∘ D₁ f ] ∘ out) ∘ ι ≈⟨ pullʳ (coalg-commutes (Terminal.! (coalgebras X) {A = record { A = X × N ; α = _≅_.from nno-iso }})) ⟩
- [ out ∘ now ∘ f , i₂ ∘ D₁ f ] ∘ (idC +₁ ι) ∘ _≅_.from nno-iso ≈⟨ (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl) ⟩
- (f +₁ D₁ f) ∘ (idC +₁ ι) ∘ _≅_.from nno-iso ≈⟨ pullˡ +₁∘+₁ ⟩
- (f ∘ idC +₁ D₁ f ∘ ι) ∘ _≅_.from nno-iso ≈⟨ ((+₁-cong₂ id-comm (sym identityʳ)) ⟩∘⟨refl) ⟩
- (idC ∘ f +₁ (D₁ f ∘ ι) ∘ idC) ∘ _≅_.from nno-iso ≈⟨ sym (pullˡ +₁∘+₁) ⟩
- (idC +₁ extend (now ∘ f) ∘ ι) ∘ (f +₁ idC) ∘ _≅_.from nno-iso ∎ })))) ⟩
- ρ ∘ extend (u (Terminal.! (coalgebras Y) {A = record { A = X × N ; α = (f +₁ idC) ∘ _≅_.from nno-iso }})) ≈⟨ (refl⟩∘⟨ (extend-≈ (Terminal.!-unique (coalgebras Y) (record { f = ι ∘ (f ⁂ idC) ; commutes = begin
- out ∘ ι ∘ (f ⁂ idC) ≈⟨ pullˡ (coalg-commutes (Terminal.! (coalgebras Y) {A = record { A = Y × N ; α = _≅_.from nno-iso }})) ⟩
- ((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (f ⁂ idC) ≈⟨ assoc ⟩
- (idC +₁ ι) ∘ _≅_.from nno-iso ∘ (f ⁂ idC) ≈⟨ (refl⟩∘⟨ (introʳ (_≅_.isoˡ nno-iso))) ⟩
- (idC +₁ ι) ∘ (_≅_.from nno-iso ∘ (f ⁂ idC)) ∘ [ ⟨ idC , z ∘ Terminal.! terminal ⟩ , idC ⁂ s ] ∘ _≅_.from nno-iso ≈⟨ (refl⟩∘⟨ pullʳ (pullˡ ∘[])) ⟩
- (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ (f ⁂ idC) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ , (f ⁂ idC) ∘ (idC ⁂ s) ] ∘ _≅_.from nno-iso ≈⟨ (refl⟩∘⟨ (refl⟩∘⟨ (([]-cong₂ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityʳ identityˡ) (⁂∘⁂ ○ ⁂-cong₂ identityʳ identityˡ)) ⟩∘⟨refl))) ⟩
- (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ ⟨ f , z ∘ Terminal.! terminal ⟩ , (f ⁂ s) ] ∘ _≅_.from nno-iso ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ refl (refl⟩∘⟨ Terminal.!-unique terminal (Terminal.! terminal ∘ f))) refl ⟩∘⟨refl) ⟩
- (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ ⟨ f , z ∘ Terminal.! terminal ∘ f ⟩ , (f ⁂ s) ] ∘ _≅_.from nno-iso ≈⟨ sym (refl⟩∘⟨ refl⟩∘⟨ []-cong₂ (⟨⟩∘ ○ ⟨⟩-cong₂ identityˡ assoc) (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ) ⟩∘⟨refl) ⟩
- (idC +₁ ι) ∘ _≅_.from nno-iso ∘ [ ⟨ idC , z ∘ Terminal.! terminal ⟩ ∘ f , (idC ⁂ s) ∘ (f ⁂ idC) ] ∘ _≅_.from nno-iso ≈⟨ sym (refl⟩∘⟨ (pullʳ (pullˡ []∘+₁))) ⟩
- (idC +₁ ι) ∘ (_≅_.from nno-iso ∘ [ ⟨ idC , z ∘ Terminal.! terminal ⟩ , idC ⁂ s ]) ∘ (f +₁ (f ⁂ idC)) ∘ _≅_.from nno-iso ≈⟨ sym (refl⟩∘⟨ introˡ (_≅_.isoʳ nno-iso)) ⟩
- (idC +₁ ι) ∘ (f +₁ (f ⁂ idC)) ∘ _≅_.from nno-iso ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ refl) ⟩
- (f +₁ ι ∘ (f ⁂ idC)) ∘ _≅_.from nno-iso ≈⟨ sym (pullˡ (+₁∘+₁ ○ +₁-cong₂ identityˡ identityʳ)) ⟩
- (idC +₁ ι ∘ (f ⁂ idC)) ∘ (f +₁ idC) ∘ _≅_.from nno-iso ∎ })))) ⟩
- ρ ∘ extend (ι ∘ (f ⁂ idC)) ≈⟨ (refl⟩∘⟨ extend-≈ (pushˡ (sym k-identityʳ))) ⟩
- ρ ∘ extend (extend ι ∘ now ∘ (f ⁂ idC)) ≈⟨ pushʳ k-assoc ⟩
- (ρ ∘ extend ι) ∘ D₁ (f ⁂ idC) ≈⟨ pushˡ (Coequalizer.equality (coeqs Y)) ⟩
- ρ ∘ D₁ π₁ ∘ D₁ (f ⁂ idC) ≈⟨ refl⟩∘⟨ sym D-homomorphism ⟩
- ρ ∘ D₁ (π₁ ∘ (f ⁂ idC)) ≈⟨ (refl⟩∘⟨ (D-resp-≈ project₁)) ⟩
- ρ ∘ D₁ (f ∘ π₁) ≈⟨ pushʳ D-homomorphism ⟩
- (ρ ∘ D₁ f) ∘ D₁ π₁ ∎)
- where
- open Coequalizer (coeqs X) using (coequalize; equality) renaming (universal to coeq-universal)
-
- ρ-natural : NaturalTransformation D-Functor Ď-Functor
- ρ-natural = ntHelper (record
- { η = λ X → ρ {X}
- ; commute = λ {X} {Y} f → Coequalizer.universal (coeqs X)
- })
-```
diff --git a/agda/src/Monad/Instance/Delay/Strong.lagda.md b/agda/src/Monad/Instance/Delay/Strong.lagda.md
index ad29f67..8b59642 100644
--- a/agda/src/Monad/Instance/Delay/Strong.lagda.md
+++ b/agda/src/Monad/Instance/Delay/Strong.lagda.md
@@ -100,7 +100,7 @@ module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : De
out ∘ extend (now ∘ π₂) ∘ τ _ ∘ idC ≈⟨ pullˡ diag₃ ⟩
((π₂ +₁ extend (now ∘ π₂)) ∘ out) ∘ τ _ ∘ idC ≈⟨ pullʳ (pullˡ (diag₂ (Terminal.⊤ terminal , X))) ⟩
(π₂ +₁ extend (now ∘ π₂)) ∘ ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ idC ≈⟨ refl⟩∘⟨ (pullʳ (assoc ○ sym diag₁)) ⟩
- (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ○ CC.+-unique ((identity² ⟩∘⟨refl) ○ id-comm-sym) ((identity² ⟩∘⟨refl) ○ id-comm-sym)) ) ⟩
+ (π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (pullˡ (+₁∘+₁ ○ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ○ []-unique ((identity² ⟩∘⟨refl) ○ id-comm-sym) ((identity² ⟩∘⟨refl) ○ id-comm-sym)) ) ⟩
(π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩
(π₂ ∘ idC +₁ extend (now ∘ π₂) ∘ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ id-comm refl) ⟩∘⟨refl ⟩
(idC ∘ π₂ +₁ extend (now ∘ π₂) ∘ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullˡ +₁∘+₁ ⟩
@@ -121,7 +121,7 @@ module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : De
diag₁ = begin
(⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩
(⟨ Terminal.! terminal , idC ⟩ ∘ π₂ +₁ idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ +₁-cong₂ (_≅_.isoˡ ⊤×A≅A) identity² ⟩∘⟨ (refl⟩∘⟨ sym identityʳ) ⟩
- (idC +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC ≈⟨ elimˡ (CC.+-unique id-comm-sym id-comm-sym) ⟩
+ (idC +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC ≈⟨ elimˡ ([]-unique id-comm-sym id-comm-sym) ⟩
distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC ∎
diag₂ = τ-law
diag₃ : out {X} ∘ extend (now ∘ π₂ {A = Terminal.⊤ terminal} {B = X}) ≈ (π₂ +₁ extend (now ∘ π₂)) ∘ out
diff --git a/agda/src/index.lagda.md b/agda/src/index.lagda.md
index 8aab6ea..a5707a8 100644
--- a/agda/src/index.lagda.md
+++ b/agda/src/index.lagda.md
@@ -35,12 +35,6 @@ open import Monad.Instance.Delay.Strong
open import Monad.Instance.Delay.Commutative
```
-The next step is to quotient the delay monad by weak bisimilarity, but this quotiented structure is not monadic, so we postulate conditions under which it extends to a monad.
-
-```agda
-open import Monad.Instance.Delay.Quotienting
-```
-
### Monad K
The goal of this last section is to formalize an equational lifting monad **K** that generalizes both the maybe monad and the delay monad.
@@ -103,7 +97,7 @@ open import Monad.Instance.K.StrongPreElgot
### A case study on setoids
Lastly we do a case study on the category of setoids.
-First we look at the (quotiented delay monad) on setoids:
+First we look at the (quotiented) delay monad on setoids:
```agda
open import Monad.Instance.Setoids.Delay