mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Worked on strength of delay
This commit is contained in:
parent
6ce2526b6a
commit
7c5dccc0ab
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 205 additions and 97 deletions
|
|
@ -9,6 +9,8 @@ open import Categories.Category.Distributive using (Distributive)
|
|||
open import Categories.Category.Cartesian using (Cartesian)
|
||||
open import Categories.Category.BinaryProducts using (BinaryProducts)
|
||||
open import Categories.Category.Cartesian.Bundle using (CartesianCategory)
|
||||
open import Categories.Category.Cartesian.Monoidal
|
||||
open import Categories.Category.Monoidal
|
||||
open import Categories.Category.Cocartesian using (Cocartesian)
|
||||
open import Categories.Object.NaturalNumbers.Parametrized using (ParametrizedNNO)
|
||||
open import Categories.Object.Exponential using (Exponential)
|
||||
|
|
@ -43,6 +45,8 @@ module Category.Instance.AmbientCategory where
|
|||
open Extensive extensive public
|
||||
open Cocartesian cocartesian renaming (+-unique to []-unique) public
|
||||
open Cartesian cartesian public
|
||||
monoidal : Monoidal C
|
||||
monoidal = CartesianMonoidal.monoidal cartesian
|
||||
-- open Terminal terminal public
|
||||
-- Don't open the terminal object, because we are interested in many different terminal objects stemming from multiple categories
|
||||
open BinaryProducts products renaming (η to ⁂-η; g-η to ⁂-g-η; unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′) public
|
||||
|
|
@ -52,6 +56,15 @@ module Category.Instance.AmbientCategory where
|
|||
distributive : Distributive C
|
||||
distributive = Extensive×Cartesian⇒Distributive C extensive cartesian
|
||||
open Distributive distributive hiding (cartesian; cocartesian) public
|
||||
open M' C
|
||||
|
||||
distributeˡ⁻¹ : ∀ {A B C : Obj} → A × (B + C) ⇒ A × B + A × C
|
||||
distributeˡ⁻¹ = IsIso.inv isIsoˡ
|
||||
|
||||
distributeʳ⁻¹ : ∀ {A B C : Obj} → (B + C) × A ⇒ B × A + C × A
|
||||
distributeʳ⁻¹ = IsIso.inv isIsoʳ
|
||||
|
||||
|
||||
|
||||
module M = M'
|
||||
module MR = MR'
|
||||
|
|
|
|||
|
|
@ -7,10 +7,12 @@ open import Categories.Object.Terminal
|
|||
open import Categories.Category.Construction.F-Coalgebras
|
||||
open import Categories.Category.Construction.F-Algebras
|
||||
open import Categories.Functor.Coalgebra
|
||||
open import Categories.Functor
|
||||
open import Categories.Functor renaming (id to idF)
|
||||
open import Categories.Functor.Algebra
|
||||
open import Categories.Monad.Construction.Kleisli
|
||||
open import Categories.Monad.Strong
|
||||
open import Categories.Category.Construction.F-Coalgebras
|
||||
open import Categories.NaturalTransformation
|
||||
open import Category.Instance.AmbientCategory using (Ambient)
|
||||
```
|
||||
-->
|
||||
|
|
@ -121,32 +123,20 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
|
|||
D₀ : Obj → Obj
|
||||
D₀ X = DX {X}
|
||||
|
||||
kleisli : KleisliTriple C
|
||||
kleisli = record
|
||||
{ F₀ = D₀
|
||||
; unit = now
|
||||
; extend = extend
|
||||
; identityʳ = identityʳ'
|
||||
; identityˡ = identityˡ'
|
||||
; assoc = assoc'
|
||||
; sym-assoc = sym assoc'
|
||||
; extend-≈ = extend-≈'
|
||||
}
|
||||
where
|
||||
open Terminal
|
||||
module _ {X Y : Obj} (f : X ⇒ D₀ Y) where
|
||||
open Terminal
|
||||
alg : F-Coalgebra (Y +-)
|
||||
alg = record { A = D₀ X + D₀ Y ; α = [ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out , (idC +₁ i₂) ∘ out ] }
|
||||
|
||||
extend : D₀ X ⇒ D₀ Y
|
||||
extend = u (! (coalgebras Y) {A = alg}) ∘ i₁ {B = D₀ Y}
|
||||
extend' : D₀ X ⇒ D₀ Y
|
||||
extend' = u (! (coalgebras Y) {A = alg}) ∘ i₁ {B = D₀ Y}
|
||||
|
||||
!∘i₂ : u (! (coalgebras Y) {A = alg}) ∘ i₂ ≈ idC
|
||||
!∘i₂ = ⊤-id (coalgebras Y) (F-Coalgebras (Y +-) [ ! (coalgebras Y) ∘ record { f = i₂ ; commutes = inject₂ } ] )
|
||||
|
||||
extendlaw : out ∘ extend ≈ [ out ∘ f , i₂ ∘ extend ] ∘ out
|
||||
extendlaw : out ∘ extend' ≈ [ out ∘ f , i₂ ∘ extend' ] ∘ out
|
||||
extendlaw = begin
|
||||
out ∘ extend ≈⟨ pullˡ (commutes (! (coalgebras Y) {A = alg})) ⟩
|
||||
out ∘ extend' ≈⟨ pullˡ (commutes (! (coalgebras Y) {A = alg})) ⟩
|
||||
((idC +₁ (u (! (coalgebras Y)))) ∘ α alg) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩
|
||||
(idC +₁ (u (! (coalgebras Y)))) ∘ [ [ i₁ , i₂ ∘ i₂ ]
|
||||
∘ (out ∘ f) , i₂ ∘ i₁ ] ∘ out ≈⟨ pullˡ ∘[] ⟩
|
||||
|
|
@ -161,11 +151,11 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
|
|||
, (i₂ ∘ (u (! (coalgebras Y)))) ∘ i₁ ] ∘ out ≈⟨ ([]-cong₂
|
||||
(elimˡ (([]-cong₂ identityʳ (cancelʳ !∘i₂)) ○ +-η))
|
||||
assoc) ⟩∘⟨refl ⟩
|
||||
[ out ∘ f , i₂ ∘ extend ] ∘ out ∎
|
||||
[ out ∘ f , i₂ ∘ extend' ] ∘ out ∎
|
||||
|
||||
extend-unique : (g : D₀ X ⇒ D₀ Y) → (out ∘ g ≈ [ out ∘ f , i₂ ∘ g ] ∘ out) → extend ≈ g
|
||||
extend-unique g g-commutes = begin
|
||||
extend ≈⟨ (!-unique (coalgebras Y) (record { f = [ g , idC ] ; commutes = begin
|
||||
extend'-unique : (g : D₀ X ⇒ D₀ Y) → (out ∘ g ≈ [ out ∘ f , i₂ ∘ g ] ∘ out) → extend' ≈ g
|
||||
extend'-unique g g-commutes = begin
|
||||
extend' ≈⟨ (!-unique (coalgebras Y) (record { f = [ g , idC ] ; commutes = begin
|
||||
out ∘ [ g , idC ] ≈⟨ ∘[] ⟩
|
||||
[ out ∘ g , out ∘ idC ] ≈⟨ []-cong₂ g-commutes identityʳ ⟩
|
||||
[ [ out ∘ f , i₂ ∘ g ] ∘ out , out ] ≈˘⟨ []-cong₂
|
||||
|
|
@ -208,6 +198,20 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
|
|||
[ g , idC ] ∘ i₁ ≈⟨ inject₁ ⟩
|
||||
g ∎
|
||||
|
||||
kleisli : KleisliTriple C
|
||||
kleisli = record
|
||||
{ F₀ = D₀
|
||||
; unit = now
|
||||
; extend = extend'
|
||||
; identityʳ = identityʳ'
|
||||
; identityˡ = identityˡ'
|
||||
; assoc = assoc'
|
||||
; sym-assoc = sym assoc'
|
||||
; extend-≈ = extend-≈'
|
||||
}
|
||||
where
|
||||
open Terminal
|
||||
|
||||
αf≈αg : ∀ {X Y} {f g : X ⇒ D₀ Y} → f ≈ g → α (alg f) ≈ α (alg g)
|
||||
αf≈αg {X} {Y} {f} {g} eq = []-cong₂ ([]-cong₂ (refl⟩∘⟨ refl⟩∘⟨ eq) refl ⟩∘⟨refl) refl
|
||||
|
||||
|
|
@ -230,18 +234,18 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
|
|||
}
|
||||
where open Functor (Y +-) using (identity)
|
||||
|
||||
identityʳ' : ∀ {X Y : Obj} {f : X ⇒ D₀ Y} → extend f ∘ now {X} ≈ f
|
||||
identityʳ' : ∀ {X Y : Obj} {f : X ⇒ D₀ Y} → extend' f ∘ now {X} ≈ f
|
||||
identityʳ' {X} {Y} {f} = begin
|
||||
extend f ∘ now ≈⟨ insertˡ (_≅_.isoˡ out-≅) ⟩∘⟨refl ⟩
|
||||
(out⁻¹ ∘ out ∘ extend f) ∘ now ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩
|
||||
(out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend f ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitlaw) ⟩
|
||||
out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend f ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩
|
||||
extend' f ∘ now ≈⟨ insertˡ (_≅_.isoˡ out-≅) ⟩∘⟨refl ⟩
|
||||
(out⁻¹ ∘ out ∘ extend' f) ∘ now ≈⟨ (refl⟩∘⟨ (extendlaw f)) ⟩∘⟨refl ⟩
|
||||
(out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend' f ] ∘ out) ∘ now ≈⟨ pullʳ (pullʳ unitlaw) ⟩
|
||||
out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend' f ] ∘ i₁ ≈⟨ refl⟩∘⟨ inject₁ ⟩
|
||||
out⁻¹ ∘ out ∘ f ≈⟨ cancelˡ (_≅_.isoˡ out-≅) ⟩
|
||||
f ∎
|
||||
|
||||
identityˡ' : ∀ {X} → extend now ≈ idC
|
||||
identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend now ; commutes = begin
|
||||
out ∘ extend now ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg now}))) ⟩
|
||||
identityˡ' : ∀ {X} → extend' now ≈ idC
|
||||
identityˡ' {X} = Terminal.⊤-id (coalgebras X) (record { f = extend' now ; commutes = begin
|
||||
out ∘ extend' now ≈⟨ pullˡ ((commutes (! (coalgebras X) {A = alg now}))) ⟩
|
||||
((idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ α (alg now)) ∘ i₁ ≈⟨ pullʳ inject₁ ⟩
|
||||
(idC +₁ (u (! (coalgebras X) {A = alg now})))
|
||||
∘ [ [ i₁ , i₂ ∘ i₂ ] ∘ (out ∘ now) , i₂ ∘ i₁ ] ∘ out ≈⟨ refl⟩∘⟨ []-cong₂ ((refl⟩∘⟨ unitlaw) ○ inject₁) refl ⟩∘⟨refl ⟩
|
||||
|
|
@ -249,21 +253,21 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
|
|||
[ (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₁
|
||||
, (idC +₁ (u (! (coalgebras X) {A = alg now}))) ∘ i₂ ∘ i₁ ] ∘ out ≈⟨ []-cong₂ +₁∘i₁ (pullˡ +₁∘i₂) ⟩∘⟨refl ⟩
|
||||
[ i₁ ∘ idC , (i₂ ∘ (u (! (coalgebras X) {A = alg now}))) ∘ i₁ ] ∘ out ≈⟨ []-cong₂ refl assoc ⟩∘⟨refl ⟩
|
||||
[ i₁ ∘ idC , i₂ ∘ (extend now) ] ∘ out ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
|
||||
([ i₁ , i₂ ] ∘ (idC +₁ extend now)) ∘ out ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩
|
||||
(idC +₁ extend now) ∘ out ∎ })
|
||||
[ i₁ ∘ idC , i₂ ∘ (extend' now) ] ∘ out ≈˘⟨ []∘+₁ ⟩∘⟨refl ⟩
|
||||
([ i₁ , i₂ ] ∘ (idC +₁ extend' now)) ∘ out ≈⟨ elimˡ +-η ⟩∘⟨refl ⟩
|
||||
(idC +₁ extend' now) ∘ out ∎ })
|
||||
|
||||
assoc' : ∀ {X Y Z : Obj} {g : X ⇒ D₀ Y} {h : Y ⇒ D₀ Z} → extend (extend h ∘ g) ≈ extend h ∘ extend g
|
||||
assoc' {X} {Y} {Z} {g} {h} = extend-unique (extend h ∘ g) (extend h ∘ extend g) (begin
|
||||
out ∘ extend h ∘ extend g ≈⟨ pullˡ (extendlaw h) ⟩
|
||||
([ out ∘ h , i₂ ∘ extend h ] ∘ out) ∘ extend g ≈⟨ pullʳ (extendlaw g) ⟩
|
||||
[ out ∘ h , i₂ ∘ extend h ] ∘ [ out ∘ g , i₂ ∘ extend g ] ∘ out ≈⟨ pullˡ ∘[] ⟩
|
||||
[ [ out ∘ h , i₂ ∘ extend h ] ∘ out ∘ g
|
||||
, [ out ∘ h , i₂ ∘ extend h ] ∘ i₂ ∘ extend g ] ∘ out ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩
|
||||
[ (out ∘ extend h) ∘ g , (i₂ ∘ extend h) ∘ extend g ] ∘ out ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨refl ⟩
|
||||
[ out ∘ extend h ∘ g , i₂ ∘ extend h ∘ extend g ] ∘ out ∎)
|
||||
assoc' : ∀ {X Y Z : Obj} {g : X ⇒ D₀ Y} {h : Y ⇒ D₀ Z} → extend' (extend' h ∘ g) ≈ extend' h ∘ extend' g
|
||||
assoc' {X} {Y} {Z} {g} {h} = extend'-unique (extend' h ∘ g) (extend' h ∘ extend' g) (begin
|
||||
out ∘ extend' h ∘ extend' g ≈⟨ pullˡ (extendlaw h) ⟩
|
||||
([ out ∘ h , i₂ ∘ extend' h ] ∘ out) ∘ extend' g ≈⟨ pullʳ (extendlaw g) ⟩
|
||||
[ out ∘ h , i₂ ∘ extend' h ] ∘ [ out ∘ g , i₂ ∘ extend' g ] ∘ out ≈⟨ pullˡ ∘[] ⟩
|
||||
[ [ out ∘ h , i₂ ∘ extend' h ] ∘ out ∘ g
|
||||
, [ out ∘ h , i₂ ∘ extend' h ] ∘ i₂ ∘ extend' g ] ∘ out ≈⟨ []-cong₂ (pullˡ (⟺ (extendlaw h))) (pullˡ inject₂) ⟩∘⟨refl ⟩
|
||||
[ (out ∘ extend' h) ∘ g , (i₂ ∘ extend' h) ∘ extend' g ] ∘ out ≈⟨ ([]-cong₂ assoc assoc) ⟩∘⟨refl ⟩
|
||||
[ out ∘ extend' h ∘ g , i₂ ∘ extend' h ∘ extend' g ] ∘ out ∎)
|
||||
|
||||
extend-≈' : ∀ {X} {Y} {f g : X ⇒ D₀ Y} → f ≈ g → extend f ≈ extend g
|
||||
extend-≈' : ∀ {X} {Y} {f g : X ⇒ D₀ Y} → f ≈ g → extend' f ≈ extend' g
|
||||
extend-≈' {X} {Y} {f} {g} eq = begin
|
||||
u (! (coalgebras Y) {A = alg f }) ∘ i₁ {B = D₀ Y} ≈⟨ (!-unique (coalgebras Y) (record { f = (u (! (coalgebras Y) {A = alg g }) ∘ idC) ; commutes = begin
|
||||
α (⊤ (coalgebras Y)) ∘ u (! (coalgebras Y)) ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
|
||||
|
|
@ -272,7 +276,7 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
|
|||
(idC +₁ u (! (coalgebras Y)) ∘ idC) ∘ α (alg f) ∎ }))
|
||||
⟩∘⟨refl ⟩
|
||||
(u (! (coalgebras Y) {A = alg g }) ∘ idC) ∘ i₁ {B = D₀ Y} ≈⟨ identityʳ ⟩∘⟨refl ⟩
|
||||
extend g ∎
|
||||
extend' g ∎
|
||||
|
||||
monad : Monad C
|
||||
monad = Kleisli⇒Monad C kleisli
|
||||
|
|
@ -281,3 +285,94 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
|
|||
functor : Endofunctor C
|
||||
functor = Monad.F monad
|
||||
```
|
||||
|
||||
Next we will show that the delay monad is strong, by giving a natural transformation `strengthen : X × DY ⇒ D (X × Y)
|
||||
|
||||
```agda
|
||||
module _ where
|
||||
open Functor
|
||||
open import Categories.Category.Monoidal.Core
|
||||
open Monoidal monoidal
|
||||
open import Categories.Monad.Relative using () renaming (Monad to RMonad)
|
||||
open RMonad kleisli using (extend)
|
||||
open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_)
|
||||
strength : Strength monoidal monad
|
||||
strength = record
|
||||
{ strengthen = ntHelper (record
|
||||
{ η = τ
|
||||
; commute = commute' })
|
||||
; identityˡ = λ {X} → begin
|
||||
extend (now ∘ π₂) ∘ τ _ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩
|
||||
(out⁻¹ ∘ out) ∘ extend (now ∘ π₂) ∘ τ _ ≈⟨ pullʳ (pullˡ (extendlaw (now ∘ π₂))) ⟩
|
||||
out⁻¹ ∘ ([ out ∘ now ∘ π₂ , i₂ ∘ extend (now ∘ π₂)] ∘ out) ∘ τ _ ≈⟨ refl⟩∘⟨ (pullʳ (τ-law (Terminal.⊤ terminal , X))) ⟩
|
||||
out⁻¹ ∘ [ out ∘ now ∘ π₂ , i₂ ∘ extend (now ∘ π₂)] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ {! refl⟩∘⟨_ !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
-- TODO extend and τ are both final coalgebras, maybe use this?
|
||||
π₂ ∎
|
||||
; η-comm = {! !}
|
||||
; μ-η-comm = {! !}
|
||||
; strength-assoc = {! !}
|
||||
}
|
||||
where
|
||||
open import Agda.Builtin.Sigma
|
||||
module _ (P : Category.Obj (CProduct C C)) where
|
||||
X = fst P
|
||||
Y = snd P
|
||||
open Terminal (coalgebras (X × Y))
|
||||
|
||||
τ : X × D₀ Y ⇒ D₀ (X × Y)
|
||||
τ = u (! {A = record { A = X × D₀ Y ; α = distributeˡ⁻¹ ∘ (idC ⁂ out) }})
|
||||
|
||||
τ-law : out ∘ τ ≈ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
|
||||
τ-law = commutes (! {A = record { A = X × D₀ Y ; α = distributeˡ⁻¹ ∘ (idC ⁂ out) }})
|
||||
|
||||
τ-unique : (t : X × D₀ Y ⇒ D₀ (X × Y)) → (out ∘ t ≈ (idC +₁ t) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) → t ≈ τ
|
||||
τ-unique t t-commutes = sym (!-unique (record { f = t ; commutes = t-commutes }))
|
||||
|
||||
commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂)
|
||||
→ τ P₂ ∘ ((fst fg) ⁂ extend (now ∘ (snd fg))) ≈ extend (now ∘ ((fst fg) ⁂ (snd fg))) ∘ τ P₁
|
||||
commute' {(U , V)} {(W , X)} (f , g) = begin
|
||||
τ _ ∘ (f ⁂ extend (now ∘ g)) ≈⟨ sym (!-unique (record { f = τ _ ∘ (f ⁂ extend (now ∘ g)) ; commutes = begin
|
||||
out ∘ τ (W , X) ∘ (f ⁂ extend (now ∘ g)) ≈⟨ pullˡ (τ-law (W , X)) ⟩
|
||||
((idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (f ⁂ extend (now ∘ g)) ≈⟨ pullʳ (pullʳ ⁂∘⁂) ⟩
|
||||
(idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (idC ∘ f ⁂ out ∘ extend (now ∘ g)) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ identityˡ (extendlaw (now ∘ g)))) ⟩
|
||||
(idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ⁂ [ out ∘ now ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ out) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ refl (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl))) ⟩
|
||||
(idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ⁂ [ i₁ ∘ g , i₂ ∘ extend (now ∘ g) ] ∘ out) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ (sym identityʳ) refl)) ⟩
|
||||
(idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ∘ idC ⁂ (g +₁ extend (now ∘ g)) ∘ out) ≈⟨ sym (pullʳ (pullʳ ⁂∘⁂)) ⟩
|
||||
((idC +₁ τ (W , X)) ∘ distributeˡ⁻¹ ∘ (f ⁂ (g +₁ extend (now ∘ g)))) ∘ (idC ⁂ out) ≈⟨ (refl⟩∘⟨ (sym (distribute₁ f g (extend (now ∘ g))))) ⟩∘⟨refl ⟩
|
||||
((idC +₁ τ (W , X)) ∘ ((f ⁂ g) +₁ (f ⁂ extend (now ∘ g))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ (pullˡ +₁∘+₁) ⟩∘⟨refl ⟩
|
||||
((idC ∘ (f ⁂ g) +₁ τ (W , X) ∘ (f ⁂ extend (now ∘ g))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ sym (((+₁-cong₂ refl identityʳ) ⟩∘⟨refl) ⟩∘⟨refl) ⟩
|
||||
((idC ∘ (f ⁂ g) +₁ (τ (W , X) ∘ (f ⁂ extend (now ∘ g))) ∘ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ sym (pullˡ (pullˡ +₁∘+₁)) ⟩
|
||||
(idC +₁ (τ (W , X) ∘ (f ⁂ extend (now ∘ g)))) ∘ ((f ⁂ g +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ∎ })) ⟩
|
||||
u ! ≈⟨ !-unique (record { f = extend (now ∘ (f ⁂ g)) ∘ τ _ ; commutes = begin
|
||||
out ∘ extend (now ∘ (f ⁂ g)) ∘ τ _ ≈⟨ pullˡ (extendlaw (now ∘ (f ⁂ g))) ⟩
|
||||
([ out ∘ now ∘ (f ⁂ g) , i₂ ∘ extend (now ∘ (f ⁂ g)) ] ∘ out) ∘ τ (U , V) ≈⟨ (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl) ⟩∘⟨refl ⟩
|
||||
([ i₁ ∘ (f ⁂ g) , i₂ ∘ extend (now ∘ (f ⁂ g)) ] ∘ out) ∘ τ (U , V) ≈⟨ pullʳ (τ-law (U , V)) ⟩
|
||||
((f ⁂ g) +₁ (extend (now ∘ (f ⁂ g)))) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ sym-assoc ⟩
|
||||
((((f ⁂ g) +₁ (extend (now ∘ (f ⁂ g)))) ∘ (idC +₁ τ _)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ (+₁∘+₁ ⟩∘⟨refl) ⟩∘⟨refl ⟩
|
||||
((((f ⁂ g) ∘ idC) +₁ (extend (now ∘ (f ⁂ g)) ∘ τ (U , V))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ sym (((+₁-cong₂ id-comm-sym identityʳ) ⟩∘⟨refl) ⟩∘⟨refl) ⟩
|
||||
(((idC ∘ (f ⁂ g)) +₁ ((extend (now ∘ (f ⁂ g)) ∘ τ (U , V)) ∘ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ sym (pullˡ (pullˡ +₁∘+₁)) ⟩
|
||||
(idC +₁ (extend (now ∘ (f ⁂ g)) ∘ τ (U , V))) ∘ (((f ⁂ g) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ∎ }) ⟩
|
||||
extend (now ∘ (f ⁂ g)) ∘ τ _ ∎
|
||||
where
|
||||
open Terminal (coalgebras (W × X))
|
||||
alg' : F-Coalgebra ((W × X) +-)
|
||||
alg' = record { A = U × D₀ V ; α = ((f ⁂ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }
|
||||
distribute₁ : ∀ {X Y Z U V W} (f : X ⇒ U) (g : Y ⇒ V) (h : Z ⇒ W) → ((f ⁂ g) +₁ (f ⁂ h)) ∘ distributeˡ⁻¹ ≈ distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h))
|
||||
distribute₁ f g h = begin
|
||||
((f ⁂ g) +₁ (f ⁂ h)) ∘ distributeˡ⁻¹ ≈⟨ introˡ (IsIso.isoˡ isIsoˡ) ⟩
|
||||
(distributeˡ⁻¹ ∘ distributeˡ) ∘ ((f ⁂ g) +₁ (f ⁂ h)) ∘ distributeˡ⁻¹ ≈⟨ pullˡ (pullʳ []∘+₁) ⟩
|
||||
(distributeˡ⁻¹ ∘ [(idC ⁂ i₁) ∘ (f ⁂ g) , (idC ⁂ i₂) ∘ (f ⁂ h)]) ∘ distributeˡ⁻¹ ≈⟨ (refl⟩∘⟨ ([]-cong₂ ⁂∘⁂ ⁂∘⁂)) ⟩∘⟨refl ⟩
|
||||
(distributeˡ⁻¹ ∘ [ idC ∘ f ⁂ i₁ ∘ g , idC ∘ f ⁂ i₂ ∘ h ]) ∘ distributeˡ⁻¹ ≈⟨ sym ((refl⟩∘⟨ ([]-cong₂ (⁂-cong₂ id-comm +₁∘i₁) (⁂-cong₂ id-comm +₁∘i₂))) ⟩∘⟨refl) ⟩
|
||||
(distributeˡ⁻¹ ∘ [ f ∘ idC ⁂ (g +₁ h) ∘ i₁ , f ∘ idC ⁂ (g +₁ h) ∘ i₂ ]) ∘ distributeˡ⁻¹ ≈˘⟨ (refl⟩∘⟨ ([]-cong₂ ⁂∘⁂ ⁂∘⁂)) ⟩∘⟨refl ⟩
|
||||
(distributeˡ⁻¹ ∘ [ ((f ⁂ (g +₁ h)) ∘ (idC ⁂ i₁)) , ((f ⁂ (g +₁ h)) ∘ (idC ⁂ i₂)) ]) ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ (pullʳ ∘[])) ⟩
|
||||
(distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h))) ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ sym (introʳ (IsIso.isoʳ isIsoˡ)) ⟩
|
||||
distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h)) ∎
|
||||
-- ⁂ ○ ˡ
|
||||
strongMonad : StrongMonad monoidal
|
||||
strongMonad = record { M = monad ; strength = strength }
|
||||
```
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue