mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
some refactoring, change ambient category
This commit is contained in:
parent
0f157442fe
commit
98837f659c
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
7 changed files with 38 additions and 302 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -1,114 +1,46 @@
|
|||
<!--
|
||||
```agda
|
||||
open import Level using (lift; Lift) renaming (suc to ℓ-suc)
|
||||
open import Level using (_⊔_) renaming (suc to ℓ-suc)
|
||||
open import Category.Ambient
|
||||
open import Categories.Category.Instance.Setoids
|
||||
open import Categories.Category.Instance.Properties.Setoids.Extensive
|
||||
open import Categories.Category.Instance.Properties.Setoids.CCC
|
||||
open import Categories.Category.Distributive
|
||||
open import Categories.Category.Monoidal.Instance.Setoids
|
||||
open import Categories.Category.Instance.SingletonSet
|
||||
open import Categories.Object.NaturalNumbers
|
||||
open import Relation.Binary
|
||||
open import Data.Unit.Polymorphic using (tt; ⊤)
|
||||
open import Data.Empty.Polymorphic using (⊥)
|
||||
open import Function.Bundles using (_⟨$⟩_) renaming (Func to _⟶_)
|
||||
open import Function.Construct.Identity as idₛ
|
||||
open import Function.Construct.Setoid renaming (setoid to _⇨_; _∙_ to _∘_)
|
||||
open import Categories.Object.NaturalNumbers.Properties.Parametrized
|
||||
open import Categories.Category.Cocartesian
|
||||
import Relation.Binary.Reasoning.Setoid as SetoidR
|
||||
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_)
|
||||
open import Function.Bundles using () renaming (Func to _⟶_)
|
||||
open import Data.Sum
|
||||
open import Data.Sum.Relation.Binary.Pointwise
|
||||
open import Data.Product
|
||||
import Categories.Morphism as M
|
||||
```
|
||||
-->
|
||||
|
||||
# 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 }
|
||||
```
|
||||
|
|
@ -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.
|
||||
|
||||
<!-- https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgXFxtYXRoYmJ7Tn0iXSxbMiwwLCJYICsgKFggXFx0aW1lcyBcXG1hdGhiYntOfSkiXSxbMCwxLCJEIFgiXSxbMiwxLCJYICsgRCBYIl0sWzAsMSwi4omFIl0sWzAsMiwiISA9OiBcXGlvdGEiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMiwzLCJvdXQiXSxbMSwzLCJGIFxcaW90YSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ== -->
|
||||
<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsNCxbMCwwLCJYIFxcdGltZXMgXFxtYXRoYmJ7Tn0iXSxbMiwwLCJYICsgKFggXFx0aW1lcyBcXG1hdGhiYntOfSkiXSxbMCwxLCJEIFgiXSxbMiwxLCJYICsgRCBYIl0sWzAsMSwi4omFIl0sWzAsMiwiISA9OiBcXGlvdGEiLDAseyJzdHlsZSI6eyJib2R5Ijp7Im5hbWUiOiJkYXNoZWQifX19XSxbMiwzLCJvdXQiXSxbMSwzLCJGIFxcaW90YSIsMCx7InN0eWxlIjp7ImJvZHkiOnsibmFtZSI6ImRhc2hlZCJ9fX1dXQ==&embed" width="575" height="304" style="border-radius: 8px; border: none;"></iframe>
|
||||
```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 ⟩
|
||||
|
|
|
|||
|
|
@ -1,159 +0,0 @@
|
|||
<!--
|
||||
```agda
|
||||
open import Level
|
||||
|
||||
open import Categories.Functor
|
||||
open import Category.Ambient using (Ambient)
|
||||
open import Categories.Monad
|
||||
open import Categories.Monad.Construction.Kleisli
|
||||
open import Categories.Monad.Relative renaming (Monad to RMonad)
|
||||
open import Data.Product using (_,_; Σ; Σ-syntax)
|
||||
open import Categories.Functor.Algebra
|
||||
open import Categories.Functor.Coalgebra
|
||||
open import Categories.Object.Terminal
|
||||
open import Categories.NaturalTransformation.Core
|
||||
```
|
||||
-->
|
||||
|
||||
```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:
|
||||
|
||||
<!-- https://q.uiver.app/#q=WzAsMyxbMCwwLCJEKFggXFx0aW1lcyBcXG1hdGhiYntOfSkiXSxbMiwwLCJEWCJdLFs0LDAsIlxcdGlsZGV7RH1YIl0sWzEsMiwiXFxyaG9fWCJdLFswLDEsIkQgXFxwaV8xIiwyLHsib2Zmc2V0IjoxfV0sWzAsMSwiXFxpb3RhXioiLDAseyJvZmZzZXQiOi0xfV1d -->
|
||||
<iframe class="quiver-embed" src="https://q.uiver.app/#q=WzAsMyxbMCwwLCJEKFggXFx0aW1lcyBcXG1hdGhiYntOfSkiXSxbMiwwLCJEWCJdLFs0LDAsIlxcdGlsZGV7RH1YIl0sWzEsMiwiXFxyaG9fWCJdLFswLDEsIkQgXFxwaV8xIiwyLHsib2Zmc2V0IjoxfV0sWzAsMSwiXFxpb3RhXioiLDAseyJvZmZzZXQiOi0xfV1d&embed" width="765" height="176" style="border-radius: 8px; border: none;"></iframe>
|
||||
|
||||
## 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)
|
||||
})
|
||||
```
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue