mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
🎨 Tidying up proofs, added small lemma
This commit is contained in:
parent
47035c1e52
commit
65d971eb68
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
7 changed files with 476 additions and 306 deletions
|
|
@ -43,4 +43,8 @@ module Algebra.Search {o ℓ e} (ambient : Ambient o ℓ e) where
|
|||
IsSearchAlgebra⇒Search-Algebra : ∀ {A} (α : F-Algebra-on functor A) → IsSearchAlgebra α → Search-Algebra
|
||||
IsSearchAlgebra⇒Search-Algebra {A} α is = record { A = A ; search-algebra-on = record { α = α ; identity₁ = identity₁ ; identity₂ = identity₂ } }
|
||||
where open IsSearchAlgebra is
|
||||
|
||||
Search-Algebra-on⇒IsSearchAlgebra : ∀ {A} → (search : Search-Algebra-on A) → IsSearchAlgebra (Search-Algebra-on.α search)
|
||||
Search-Algebra-on⇒IsSearchAlgebra {A} search = record { identity₁ = identity₁ ; identity₂ = identity₂ }
|
||||
where open Search-Algebra-on search
|
||||
```
|
||||
|
|
@ -10,7 +10,9 @@ 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.Cartesian.SymmetricMonoidal using () renaming (symmetric to symm)
|
||||
open import Categories.Category.Monoidal
|
||||
open import Categories.Category.Monoidal.Symmetric
|
||||
open import Categories.Category.Cocartesian using (Cocartesian)
|
||||
open import Categories.Object.NaturalNumbers.Parametrized using (ParametrizedNNO)
|
||||
open import Categories.Object.Exponential using (Exponential)
|
||||
|
|
@ -47,8 +49,10 @@ module Category.Instance.AmbientCategory where
|
|||
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
|
||||
|
||||
symmetric : Symmetric monoidal
|
||||
symmetric = symm C cartesian
|
||||
|
||||
open BinaryProducts products renaming (η to ⁂-η; g-η to ⁂-g-η; unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′) public
|
||||
open ParametrizedNNO ℕ public renaming (η to pnno-η)
|
||||
|
||||
|
|
|
|||
35
src/Monad/Commutative.agda
Normal file
35
src/Monad/Commutative.agda
Normal file
|
|
@ -0,0 +1,35 @@
|
|||
{-# OPTIONS --without-K --safe #-}
|
||||
|
||||
-- Commutative Monad on a symmetric monoidal category
|
||||
-- https://ncatlab.org/nlab/show/commutative+monad
|
||||
|
||||
module Monad.Commutative where
|
||||
|
||||
open import Level
|
||||
open import Data.Product using (_,_)
|
||||
|
||||
open import Categories.Category.Core
|
||||
open import Categories.Category.Monoidal
|
||||
open import Categories.Category.Monoidal.Symmetric
|
||||
open import Categories.Monad
|
||||
open import Categories.Monad.Strong
|
||||
|
||||
private
|
||||
variable
|
||||
o ℓ e : Level
|
||||
|
||||
record CommutativeMonad {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) (T : StrongMonad V) : Set (o ⊔ ℓ ⊔ e) where
|
||||
open Category C
|
||||
open Symmetric S
|
||||
open StrongMonad T
|
||||
|
||||
|
||||
private
|
||||
σ : ∀ {X Y} → X ⊗₀ M.F.₀ Y ⇒ M.F.₀ (X ⊗₀ Y)
|
||||
σ {X} {Y} = strengthen.η (X , Y)
|
||||
|
||||
τ : ∀ {X Y} → M.F.₀ X ⊗₀ Y ⇒ M.F.₀ (X ⊗₀ Y)
|
||||
τ {X} {Y} = M.F.₁ (braiding.⇐.η (X , Y)) ∘ σ ∘ braiding.⇒.η (M.F.₀ X , Y)
|
||||
|
||||
field
|
||||
commutes : ∀ {X Y} → M.μ.η (X ⊗₀ Y) ∘ M.F.₁ τ ∘ σ ≈ M.μ.η (X ⊗₀ Y) ∘ M.F.₁ σ ∘ τ
|
||||
|
|
@ -14,6 +14,7 @@ open import Categories.Monad.Strong
|
|||
open import Categories.Category.Construction.F-Coalgebras
|
||||
open import Categories.NaturalTransformation
|
||||
open import Category.Instance.AmbientCategory using (Ambient)
|
||||
open import Monad.Commutative
|
||||
```
|
||||
-->
|
||||
```agda
|
||||
|
|
@ -204,6 +205,35 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
|
|||
[ g , idC ] ∘ i₁ ≈⟨ inject₁ ⟩
|
||||
g ∎
|
||||
|
||||
-- Lemma 39: ▷ ∘ f* ≈ (▷ ∘ f)* ≈ f* ∘ ▷
|
||||
|
||||
module _ {X Y} (f : X ⇒ D₀ Y) where
|
||||
private
|
||||
helper : out ∘ [ f , extend' (▷ ∘ f) ] ∘ out ≈ [ out ∘ f , i₂ ∘ [ f , extend' (▷ ∘ f) ] ∘ out ] ∘ out
|
||||
helper = pullˡ ∘[] ○ (([]-cong₂ refl (extendlaw (▷ ∘ f) ○ ((([]-cong₂ (pullˡ laterlaw) refl) ⟩∘⟨refl) ○ sym (pullˡ ∘[])))) ⟩∘⟨refl)
|
||||
helper₁ : [ f , extend' (▷ ∘ f) ] ∘ out ≈ extend' f
|
||||
helper₁ = sym (extend'-unique f ([ f , extend' (▷ ∘ f) ] ∘ out) helper)
|
||||
|
||||
▷∘extendˡ : ▷ ∘ extend' f ≈ extend' (▷ ∘ f)
|
||||
▷∘extendˡ = sym (begin
|
||||
extend' (▷ ∘ f) ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩
|
||||
(out⁻¹ ∘ out) ∘ extend' (▷ ∘ f) ≈⟨ pullʳ (extendlaw (▷ ∘ f)) ⟩
|
||||
out⁻¹ ∘ [ out ∘ ▷ ∘ f , i₂ ∘ extend' (▷ ∘ f) ] ∘ out ≈⟨ (refl⟩∘⟨ (([]-cong₂ (pullˡ laterlaw) refl) ○ (sym ∘[])) ⟩∘⟨refl) ⟩
|
||||
out⁻¹ ∘ (i₂ ∘ [ f , extend' (▷ ∘ f) ]) ∘ out ≈⟨ (refl⟩∘⟨ (pullʳ helper₁)) ⟩
|
||||
out⁻¹ ∘ i₂ ∘ extend' f ≈⟨ sym-assoc ⟩
|
||||
▷ ∘ extend' f ∎)
|
||||
|
||||
▷∘extend-comm : ▷ ∘ extend' f ≈ extend' f ∘ ▷
|
||||
▷∘extend-comm = sym (begin
|
||||
extend' f ∘ ▷ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩
|
||||
(out⁻¹ ∘ out) ∘ extend' f ∘ ▷ ≈⟨ pullʳ (pullˡ (extendlaw f)) ⟩
|
||||
out⁻¹ ∘ ([ out ∘ f , i₂ ∘ extend' f ] ∘ out) ∘ ▷ ≈⟨ (refl⟩∘⟨ pullʳ laterlaw) ⟩
|
||||
out⁻¹ ∘ [ out ∘ f , i₂ ∘ extend' f ] ∘ i₂ ≈⟨ (refl⟩∘⟨ inject₂) ○ sym-assoc ⟩
|
||||
▷ ∘ extend' f ∎)
|
||||
|
||||
▷∘extendʳ : extend' f ∘ ▷ ≈ extend' (▷ ∘ f)
|
||||
▷∘extendʳ = (sym ▷∘extend-comm) ○ ▷∘extendˡ
|
||||
|
||||
kleisli : KleisliTriple C
|
||||
kleisli = record
|
||||
{ F₀ = D₀
|
||||
|
|
@ -291,270 +321,3 @@ 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; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
|
||||
open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_)
|
||||
open Monad monad using () renaming (η to η'; μ to μ')
|
||||
module η = NaturalTransformation η'
|
||||
module μ = NaturalTransformation μ'
|
||||
strength : Strength monoidal monad
|
||||
strength = record
|
||||
{ strengthen = ntHelper (record
|
||||
{ η = τ
|
||||
; commute = commute' })
|
||||
; identityˡ = identityˡ' -- triangle
|
||||
; η-comm = begin -- η-τ
|
||||
τ _ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂) ⟩
|
||||
τ _ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullˡ (τ-helper _) ⟩
|
||||
(out⁻¹ ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullʳ (pullʳ dstr-law₁) ⟩
|
||||
out⁻¹ ∘ (idC +₁ τ _) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩
|
||||
out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
|
||||
now ∎
|
||||
; μ-η-comm = μ-η-comm' -- μ-τ
|
||||
; strength-assoc = strength-assoc' -- square
|
||||
}
|
||||
where
|
||||
open import Agda.Builtin.Sigma
|
||||
out-law : ∀ {X Y} (f : X ⇒ Y) → out {Y} ∘ extend (now ∘ f) ≈ (f +₁ extend (now ∘ f)) ∘ out {X}
|
||||
out-law {X} {Y} f = begin
|
||||
out ∘ extend (now ∘ f) ≈⟨ extendlaw (now ∘ f) ⟩
|
||||
[ out ∘ now ∘ f , i₂ ∘ extend (now ∘ f) ] ∘ out ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩
|
||||
(f +₁ extend (now ∘ f)) ∘ out ∎
|
||||
dstr-law₁ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₁) ≈ i₁
|
||||
dstr-law₁ = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ))
|
||||
dstr-law₂ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₂) ≈ i₂
|
||||
dstr-law₂ = (refl⟩∘⟨ (sym inject₂)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ))
|
||||
|
||||
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) }})
|
||||
|
||||
τ-helper : τ ∘ (idC ⁂ out⁻¹) ≈ out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹
|
||||
τ-helper = begin
|
||||
τ ∘ (idC ⁂ out⁻¹) ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩
|
||||
(out⁻¹ ∘ out) ∘ τ ∘ (idC ⁂ out⁻¹) ≈⟨ pullʳ (pullˡ τ-law) ⟩
|
||||
out⁻¹ ∘ ((idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ out⁻¹) ≈⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ assoc) ⟩
|
||||
out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ (idC ⁂ out⁻¹) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimʳ (⁂∘⁂ ○ (⁂-cong₂ identity² (_≅_.isoʳ out-≅)) ○ ((⟨⟩-cong₂ identityˡ identityˡ) ○ ⁂-η)))) ⟩
|
||||
out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∎
|
||||
|
||||
τ-now : τ ∘ (idC ⁂ now) ≈ now
|
||||
τ-now = begin
|
||||
τ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ (⁂-cong₂ identity² refl)) ⟩
|
||||
τ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullˡ τ-helper ⟩
|
||||
(out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullʳ (pullʳ dstr-law₁) ⟩
|
||||
out⁻¹ ∘ (idC +₁ τ) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩
|
||||
out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
|
||||
now ∎
|
||||
|
||||
τ-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 }))
|
||||
|
||||
identityˡ' : ∀ {X : Obj} → extend (now ∘ π₂) ∘ τ (Terminal.⊤ terminal , X) ≈ π₂
|
||||
identityˡ' {X} = begin
|
||||
extend (now ∘ π₂) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras X) {A = record { A = Terminal.⊤ terminal × D₀ X ; α = (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }} (record { f = extend (now ∘ π₂) ∘ τ _ ; commutes = begin
|
||||
out ∘ extend (now ∘ π₂) ∘ τ _ ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (sym identityʳ)) ⟩
|
||||
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 +₁ τ _) ∘ (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ˡ +₁∘+₁ ⟩
|
||||
(idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimˡ identity²)) ⟩
|
||||
(idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ refl⟩∘⟨ ((+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl) ⟩
|
||||
(idC +₁ extend (now ∘ π₂)) ∘ (idC ∘ π₂ +₁ τ _ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullʳ (pullˡ +₁∘+₁) ⟩
|
||||
((idC +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _)) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ (homomorphism (X +-)) ⟩∘⟨refl ⟩
|
||||
(idC +₁ extend (now ∘ π₂) ∘ τ _) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩
|
||||
u (Terminal.! (coalgebras X)) ≈⟨ Terminal.!-unique (coalgebras X) {A = record { A = Terminal.⊤ terminal × D₀ X ; α = (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }} (record { f = π₂ ; commutes = begin
|
||||
out ∘ π₂ ≈˘⟨ π₂∘⁂ ⟩
|
||||
π₂ ∘ (idC ⁂ out) ≈˘⟨ pullˡ distribute₂ ⟩ -- TODO this might be wrong if distribute₂ is unprovable
|
||||
(π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ (+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl ⟩
|
||||
(idC ∘ π₂ +₁ π₂ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullˡ +₁∘+₁ ⟩
|
||||
(idC +₁ π₂) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩
|
||||
π₂ ∎
|
||||
where
|
||||
diag₁ : (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈ distributeˡ⁻¹ {Terminal.⊤ terminal} {X} {D₀ X} ∘ (idC ⁂ out) ∘ idC
|
||||
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) ⟩
|
||||
distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC ∎
|
||||
diag₂ = τ-law
|
||||
diag₃ : out {X} ∘ extend (now ∘ π₂ {A = Terminal.⊤ terminal} {B = X}) ≈ (π₂ +₁ extend (now ∘ π₂)) ∘ out
|
||||
diag₃ = out-law π₂
|
||||
distribute₂ : ∀ {A B C} → (π₂ +₁ π₂) ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₂
|
||||
distribute₂ = sym (begin
|
||||
π₂ ≈⟨ introʳ (IsIso.isoʳ isIsoˡ) ⟩
|
||||
π₂ ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ pullˡ ∘[] ⟩
|
||||
[ π₂ ∘ ((idC ⁂ i₁)) , π₂ ∘ (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ π₂∘⁂ π₂∘⁂) ⟩∘⟨refl ⟩
|
||||
(π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∎)
|
||||
|
||||
μ-η-comm' : ∀ {X Y} → extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈ τ (X , Y) ∘ (idC ⁂ extend idC)
|
||||
μ-η-comm' {X} {Y} = begin
|
||||
extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y)) (record { f = extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ; commutes = begin
|
||||
out ∘ extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _ ≈⟨ refl⟩∘⟨ (pullˡ id*∘Dτ) ⟩
|
||||
out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ square ⟩
|
||||
[ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ sym-assoc ○ (assoc ○ tri) ⟩∘⟨refl ⟩
|
||||
((idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩
|
||||
(idC +₁ (extend (τ _) ∘ τ _)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ refl (sym (pullˡ id*∘Dτ))) ⟩∘⟨refl ⟩
|
||||
(idC +₁ (extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩
|
||||
u (Terminal.! (coalgebras (X × Y)) {A = record { A = X × D₀ (D₀ Y) ; α = [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }}) ≈⟨ Terminal.!-unique (coalgebras (X × Y)) (record { f = τ _ ∘ (idC ⁂ extend idC) ; commutes = begin
|
||||
out ∘ τ _ ∘ (idC ⁂ extend idC) ≈⟨ pullˡ (τ-law (X , Y)) ⟩
|
||||
((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ extend idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out ∘ extend idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (extendlaw idC) ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out ∘ idC , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (([]-cong₂ identityʳ refl) ⟩∘⟨refl) ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ pullˡ (assoc ○ tri₂) ⟩
|
||||
((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩
|
||||
(idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩
|
||||
τ _ ∘ (idC ⁂ extend idC) ∎
|
||||
where
|
||||
-- diagram: https://q.uiver.app/#q=WzAsNyxbMCwwLCJYXFx0aW1lcyBERFkiXSxbMiwwLCJEKFhcXHRpbWVzIERZKSJdLFs0LDAsIkREKFhcXHRpbWVzIFkpIl0sWzAsMiwiWFxcdGltZXMgKERZK0REWSkiXSxbMiwyLCJYXFx0aW1lcyBEWSsgWFxcdGltZXMgRERZIl0sWzQsMiwiWFxcdGltZXMgWSsgREQoWFxcdGltZXMgWSkiXSxbMCw0LCJYXFx0aW1lcyBZKyBYXFx0aW1lcyBERFkiXSxbMCwzLCJpZFxcdGltZXMgb3V0IiwyXSxbMCwxLCJcXHRhdSJdLFsxLDIsIlxcdGF1XioiXSxbMyw0LCIoaWQrXFx0YXUpZGlzdCJdLFs0LDUsIltvdXRcXHRhdSxpbnJcXHRhdV4qXSJdLFsyLDUsIm91dCJdLFsxLDRdLFs2LDUsImlkK1xcdGF1XipcXHRhdSIsMl0sWzMsNiwiWyhpZCArIGlkXFx0aW1lcyBub3cpZGlzdCAoaWRcXHRpbWVzIG91dCksaW5yXWRpc3QiLDJdXQ==
|
||||
square : out ∘ extend (τ (X , Y)) ∘ τ _ ≈ [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
|
||||
square = begin
|
||||
out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ pullˡ (extendlaw (τ (X , Y))) ⟩
|
||||
([ out ∘ τ (X , Y) , i₂ ∘ extend (τ (X , Y)) ] ∘ out) ∘ τ _ ≈⟨ pullʳ (τ-law _) ⟩
|
||||
[ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎
|
||||
tri : [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈ (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹
|
||||
tri = begin
|
||||
[ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈⟨ pullˡ []∘+₁ ⟩
|
||||
[ (out ∘ τ _) ∘ idC , (i₂ ∘ extend (τ (X , Y))) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ (identityʳ ○ τ-law (X , Y)) assoc) ⟩∘⟨refl ⟩
|
||||
[ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ (X , Y)) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ refl k-identityʳ) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩
|
||||
[ (idC +₁ extend (τ _) ∘ now) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ identity² (pullʳ (τ-now (X , D₀ Y)))) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩
|
||||
[ (idC ∘ idC +₁ (extend (τ _) ∘ τ _) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ (pullˡ +₁∘+₁) +₁∘i₂) ⟩∘⟨refl) ⟩
|
||||
[ (idC +₁ extend (τ _) ∘ τ _) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ extend (τ _) ∘ τ _) ∘ i₂ ] ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ ∘[]) ⟩
|
||||
(idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∎
|
||||
id*∘Dτ : extend idC ∘ extend (now ∘ τ _) ≈ extend (τ _)
|
||||
id*∘Dτ = begin
|
||||
extend idC ∘ extend (now ∘ τ _) ≈⟨ sym k-assoc ⟩
|
||||
extend (extend idC ∘ now ∘ τ _) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩
|
||||
extend (idC ∘ τ _) ≈⟨ extend-≈ identityˡ ⟩
|
||||
extend (τ _) ∎
|
||||
tri₂' : (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ
|
||||
tri₂' = begin
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ∘[]) ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₁) , (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []-cong₂ ⁂∘⁂ ⁂∘⁂ ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ (idC ∘ idC ⁂ [ out , i₂ ∘ extend idC ] ∘ i₁) , (idC ∘ idC ⁂ [ out , i₂ ∘ extend idC ] ∘ i₂) ] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []-cong₂ (⁂-cong₂ identity² inject₁) (⁂-cong₂ identity² inject₂) ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ idC ⁂ out , idC ⁂ i₂ ∘ extend idC ] ≈⟨ refl⟩∘⟨ ∘[] ⟩
|
||||
(idC +₁ τ _) ∘ [ distributeˡ⁻¹ ∘ (idC ⁂ out) , distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ ∘[] ⟩
|
||||
[ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ sym ([]-cong₂ refl (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩
|
||||
[ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂)) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl ((refl⟩∘⟨ dstr-law₂) ⟩∘⟨refl) ⟩
|
||||
[ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ _) ∘ i₂) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl (pushˡ +₁∘i₂) ⟩
|
||||
[ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((+₁-cong₂ refl (introʳ (⟨⟩-unique id-comm (id-comm ○ (sym k-identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) refl ⟩
|
||||
[ (idC +₁ τ _ ∘ (idC ⁂ extend idC ∘ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((sym (+₁-cong₂ refl (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩∘⟨refl) refl ⟩
|
||||
[ (idC +₁ τ _ ∘ (idC ⁂ extend idC) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ sym ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² assoc)) +₁∘i₂) ⟩
|
||||
[ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ i₂ ] ≈⟨ sym ∘[] ⟩
|
||||
(idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ≈⟨ sym (refl⟩∘⟨ (elimʳ (IsIso.isoˡ isIsoˡ))) ⟩
|
||||
(idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ ∎
|
||||
tri₂ : (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ≈ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹
|
||||
tri₂ = iso-epi-from
|
||||
(record { from = distributeˡ ; to = distributeˡ⁻¹ ; iso = IsIso.iso isIsoˡ })
|
||||
((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]))
|
||||
((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹)
|
||||
(assoc ○ refl⟩∘⟨ assoc ○ tri₂' ○ sym-assoc ○ sym-assoc ○ assoc ⟩∘⟨refl)
|
||||
|
||||
strength-assoc' : ∀ {X Y Z} → extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ ((X × Y), Z) ≈ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩
|
||||
strength-assoc' {X} {Y} {Z} = begin
|
||||
extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y × Z)) (record { f = extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ; commutes = begin
|
||||
out ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ pullˡ (extendlaw (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ⟩
|
||||
([ out ∘ now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , i₂ ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ] ∘ out) ∘ τ _ ≈⟨ pullʳ (τ-law (X × Y , Z)) ⟩
|
||||
[ out ∘ now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , i₂ ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩
|
||||
(⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩
|
||||
(⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ idC +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ id-comm (sym identityʳ)) ⟩∘⟨refl ⟩
|
||||
(idC ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ (extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym (pullˡ +₁∘+₁) ⟩
|
||||
(idC +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩
|
||||
u (Terminal.! (coalgebras (X × Y × Z)) {A = record { A = (X × Y) × D₀ Z ; α = (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }}) ≈⟨ Terminal.!-unique (coalgebras (X × Y × Z)) (record { f = τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ; commutes = begin
|
||||
out ∘ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullˡ (τ-law (X , Y × Z)) ⟩
|
||||
((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullʳ (pullˡ (pullʳ ⁂∘⁂)) ⟩
|
||||
(idC +₁ τ _) ∘ (distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ out ∘ τ _)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ assoc ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ out ∘ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ identityʳ (assoc ○ sym (τ-law (Y , Z)))) ⟩∘⟨refl) ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ ((idC ∘ idC) ∘ idC ⁂ ((idC +₁ τ _) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ sym (refl⟩∘⟨ (pullʳ (pullˡ ⁂∘⁂ ○ pullˡ ⁂∘⁂))) ⟩
|
||||
(idC +₁ τ _) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ _))) ∘ (idC ⁂ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (refl⟩∘⟨ helper₁)) ⟩
|
||||
(idC +₁ τ _) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ _))) ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (helper₂ ⟩∘⟨refl) ⟩
|
||||
(idC +₁ τ _) ∘ ((idC +₁ (idC ⁂ τ (Y , Z))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ sym assoc²') ⟩
|
||||
(idC +₁ τ _) ∘ (idC +₁ (idC ⁂ τ (Y , Z))) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ out) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl) ⟩
|
||||
(idC +₁ τ _ ∘ (idC ⁂ τ (Y , Z))) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (helper₃ ⟩∘⟨refl) ⟩
|
||||
(idC +₁ τ _ ∘ (idC ⁂ τ (Y , Z))) ∘ ((⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc²'' ⟩
|
||||
((idC +₁ τ _ ∘ (idC ⁂ τ _)) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym ((+₁-cong₂ refl (identityʳ ○ sym-assoc) ○ sym +₁∘+₁) ⟩∘⟨refl) ⟩
|
||||
(idC ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ (τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym (pullˡ +₁∘+₁) ⟩
|
||||
(idC +₁ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩
|
||||
τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎
|
||||
where
|
||||
helper₁ : (idC ⁂ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC {X × Y} ⁂ out {Z})
|
||||
helper₁ = begin
|
||||
(idC ⁂ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ ⁂∘⟨⟩ ⟩
|
||||
⟨ idC ∘ π₁ ∘ π₁ , (idC ⁂ out) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ identityˡ ⁂∘⟨⟩ ⟩
|
||||
⟨ π₁ ∘ π₁ , ⟨ idC ∘ π₂ ∘ π₁ , out ∘ π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ refl (⟨⟩-cong₂ identityˡ refl) ⟩
|
||||
⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , out ∘ π₂ ⟩ ⟩ ≈⟨ sym (⟨⟩-cong₂ refl (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) refl)) ⟩
|
||||
⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ idC ∘ π₁ , out ∘ π₂ ⟩ ⟩ ≈⟨ sym (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)) ⟩
|
||||
⟨ π₁ ∘ idC ∘ π₁ , ⟨ (π₂ ∘ π₁) ∘ (idC {X × Y} ⁂ out {Z}) , π₂ ∘ (idC {X × Y} ⁂ out {Z}) ⟩ ⟩ ≈⟨ sym (⟨⟩-cong₂ (pullʳ project₁) ⟨⟩∘) ⟩
|
||||
⟨ (π₁ ∘ π₁) ∘ (idC {X × Y} ⁂ out {Z}) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC {X × Y} ⁂ out {Z}) ⟩ ≈⟨ sym ⟨⟩∘ ⟩
|
||||
⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC {X × Y} ⁂ out {Z}) ∎
|
||||
helper₂ : distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ _)) ≈ (idC +₁ (idC ⁂ τ (Y , Z))) ∘ distributeˡ⁻¹
|
||||
helper₂ = sym (distribute₁ idC idC (τ _)) ○ (+₁-cong₂ (⟨⟩-unique id-comm id-comm) refl) ⟩∘⟨refl
|
||||
helper₃ : distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹
|
||||
helper₃ = sym (begin
|
||||
(⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹ ≈⟨ introˡ (IsIso.isoˡ isIsoˡ) ⟩
|
||||
(distributeˡ⁻¹ ∘ distributeˡ) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹ ≈⟨ pullʳ (pullˡ []∘+₁) ⟩
|
||||
distributeˡ⁻¹ ∘ [ (idC ⁂ i₁) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , (idC ⁂ i₂) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ (([]-cong₂ ⁂∘⟨⟩ ⁂∘⟨⟩) ⟩∘⟨refl) ⟩
|
||||
distributeˡ⁻¹ ∘ [ ⟨ idC ∘ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , ⟨ idC ∘ π₁ ∘ π₁ , i₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ identityˡ (pushˡ (sym dstr-law₁))) (⟨⟩-cong₂ identityˡ ((pushˡ (sym dstr-law₂)))) ⟩∘⟨refl ⟩
|
||||
distributeˡ⁻¹ ∘ [ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₁) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₂) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ refl (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ ○ sym identityˡ) refl ○ sym ⁂∘⟨⟩))) (⟨⟩-cong₂ refl (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ ○ sym identityˡ) refl ○ sym ⁂∘⟨⟩))) ⟩∘⟨refl) ⟩
|
||||
distributeˡ⁻¹ ∘ [ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ , ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ (identityˡ ○ refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂))) (⟨⟩-cong₂ (identityˡ ○ refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂))) ⟩∘⟨refl) ⟩
|
||||
distributeˡ⁻¹ ∘ [ ⟨ idC ∘ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₁) , π₂ ∘ (idC ⁂ i₁) ⟩ ⟩ , ⟨ idC ∘ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₂) , π₂ ∘ (idC ⁂ i₂) ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ (pullʳ (pullʳ π₁∘⁂)) (pullʳ ⟨⟩∘)) (⟨⟩-cong₂ (pullʳ (pullʳ π₁∘⁂)) (pullʳ ⟨⟩∘)) ⟩∘⟨refl) ⟩
|
||||
distributeˡ⁻¹ ∘ [ ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ i₁) , (distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ i₁) ⟩ , ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ i₂) , (distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ i₂) ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ ⟨⟩∘ ⟨⟩∘ ⟩∘⟨refl) ⟩
|
||||
distributeˡ⁻¹ ∘ [ (⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ i₁)) , (⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ i₂)) ] ∘ distributeˡ⁻¹ ≈˘⟨ pullʳ (pullˡ ∘[]) ⟩
|
||||
(distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ sym (introʳ (IsIso.isoʳ isIsoˡ)) ⟩
|
||||
distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ sym (refl⟩∘⟨ ⁂∘⟨⟩) ⟩
|
||||
distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎)
|
||||
-- {- ⁂ ⊤ ○
|
||||
-- Diagram for identityˡ':
|
||||
-- https://q.uiver.app/#q=WzAsOSxbMCwyLCIxIFxcdGltZXMgREIiXSxbMiwyLCIxIFxcdGltZXMgKEIgKyBEQikiXSxbNiwyLCIxIFxcdGltZXMgQiArIDEgXFx0aW1lcyBEQiJdLFswLDQsIkQoMSBcXHRpbWVzIEIpIl0sWzYsNCwiKDEgXFx0aW1lcyBCKSArIEQoMSBcXHRpbWVzIEIpIl0sWzAsNiwiREIiXSxbNiw2LCJCICsgREIiXSxbMCwwLCIxIFxcdGltZXMgREIiXSxbNiwwLCJCICsgMSBcXHRpbWVzIERCIl0sWzAsMSwiaWQgXFx0aW1lcyBvdXQiXSxbMSwyLCJkaXN0cmliXnstMX0iXSxbMCwzLCJcXHRhdSIsMl0sWzUsNiwib3V0IiwyXSxbMyw0LCJvdXQiLDJdLFsyLDQsImlkICsgXFx0YXUiXSxbMyw1LCJEIFxccGlfMiJdLFs0LDYsIlxccGlfMiArIEQgXFxwaV8yIl0sWzcsOCwiKFxccGlfMiArIGlkKSBcXGNpcmMgZGlzdHJpYl57LTF9IFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpIl0sWzcsMCwiaWQiXSxbOCwyLCJcXGxhbmdsZSAhICwgaWQgXFxyYW5nbGUgKyBpZCJdXQ==
|
||||
-- -}
|
||||
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) }
|
||||
|
||||
strongMonad : StrongMonad monoidal
|
||||
strongMonad = record { M = monad ; strength = strength }
|
||||
```
|
||||
|
|
|
|||
32
src/Monad/Instance/Delay/Commutative.lagda.md
Normal file
32
src/Monad/Instance/Delay/Commutative.lagda.md
Normal file
|
|
@ -0,0 +1,32 @@
|
|||
<!--
|
||||
```agda
|
||||
open import Level
|
||||
|
||||
open import Categories.Category.Core
|
||||
open import Categories.Functor
|
||||
open import Category.Instance.AmbientCategory
|
||||
open import Monad.Commutative
|
||||
open import Monad.Instance.Delay
|
||||
open import Categories.Monad
|
||||
open import Categories.Monad.Strong
|
||||
open import Categories.Monad.Relative renaming (Monad to RMonad)
|
||||
```
|
||||
-->
|
||||
|
||||
```agda
|
||||
module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D : DelayM ambient) where
|
||||
open Ambient ambient
|
||||
open DelayM D
|
||||
open import Monad.Instance.Delay.Strong ambient D
|
||||
open Functor
|
||||
open Monoidal monoidal
|
||||
open RMonad kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
|
||||
open Monad monad using (η; μ)
|
||||
```
|
||||
|
||||
# The Delay Monad is commutative
|
||||
|
||||
```agda
|
||||
commutativeMonad : CommutativeMonad symmetric strongMonad
|
||||
commutativeMonad = record { commutes = {! !} }
|
||||
```
|
||||
|
|
@ -36,7 +36,7 @@ module Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) whe
|
|||
|
||||
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 Monad D-Monad using (μ; η) renaming (assoc to M-assoc; identityʳ to M-identityʳ)
|
||||
open HomReasoning
|
||||
open M C
|
||||
open MR C
|
||||
|
|
@ -80,15 +80,42 @@ module Monad.Instance.Delay.Properties {o ℓ e} (ambient : Ambient o ℓ e) whe
|
|||
|
||||
2⇒3 : cond-2 → cond-3
|
||||
2⇒3 c-2 X = record
|
||||
{ elgot = {! !}
|
||||
{ elgot = Elgot-Algebra.algebra (D-Algebra+Search⇒Elgot D (record
|
||||
{ A = Ď₀ X
|
||||
; action = α
|
||||
; commute = epi-DDρ (α ∘ D₁ α) (α ∘ extend (idC)) (sym (begin
|
||||
(α ∘ μ.η (Ď₀ X)) ∘ D₁ (D₁ ρ) ≈⟨ pullʳ (μ.commute ρ) ⟩
|
||||
α ∘ D₁ ρ ∘ μ.η (D₀ X) ≈⟨ pullˡ (sym ρ-algebra-morphism) ⟩
|
||||
(ρ ∘ μ.η X) ∘ μ.η (D₀ X) ≈⟨ pullʳ μ∘Dμ ⟩
|
||||
ρ ∘ μ.η X ∘ D₁ (μ.η X) ≈⟨ pullˡ ρ-algebra-morphism ⟩
|
||||
(α ∘ D₁ ρ) ∘ D₁ (μ.η X) ≈⟨ pullʳ (sym D-homomorphism) ⟩
|
||||
α ∘ D₁ (ρ ∘ μ.η X) ≈⟨ (refl⟩∘⟨ (D-resp-≈ ρ-algebra-morphism)) ⟩
|
||||
α ∘ D₁ (α ∘ D₁ ρ) ≈⟨ (refl⟩∘⟨ D-homomorphism) ⟩
|
||||
α ∘ D₁ α ∘ D₁ (D₁ ρ) ≈⟨ sym-assoc ⟩
|
||||
(α ∘ D₁ α) ∘ D₁ (D₁ ρ) ∎))
|
||||
; identity = identity₁
|
||||
}) (Search-Algebra-on⇒IsSearchAlgebra D s-alg-on))
|
||||
; isFO = {! !}
|
||||
; isStable = {! !}
|
||||
; ρ-algebra-morphism = {! !}
|
||||
; ρ-law = {! !}
|
||||
}
|
||||
where
|
||||
open cond-2' (c-2 X)
|
||||
open Search-Algebra-on s-alg-on
|
||||
epi-DDρ : Epi (D₁ (D₁ ρ))
|
||||
epi-DDρ = {! !}
|
||||
μ∘Dμ : ∀ {X} → μ.η X ∘ μ.η (D₀ X) ≈ μ.η X ∘ D₁ (μ.η X)
|
||||
μ∘Dμ {X} = begin
|
||||
μ.η X ∘ μ.η (D₀ X) ≈⟨ sym k-assoc ⟩
|
||||
extend (extend idC ∘ idC) ≈⟨ extend-≈ identityʳ ⟩
|
||||
extend (extend idC) ≈⟨ extend-≈ (introˡ k-identityʳ) ⟩
|
||||
extend ((extend idC ∘ now) ∘ extend idC) ≈⟨ extend-≈ assoc ⟩
|
||||
extend (extend idC ∘ now ∘ extend idC) ≈⟨ k-assoc ⟩
|
||||
μ.η X ∘ D₁ (μ.η X) ∎
|
||||
|
||||
1⇒2 : cond-1 → cond-2
|
||||
1⇒2 c-1 X = record { s-alg-on = s-alg-on ; ρ-algebra-morphism = begin ρ ∘ μ.η X ≈⟨ D-universal ⟩ Search-Algebra-on.α s-alg-on ∘ D₁ ρ ∎ }
|
||||
1⇒2 c-1 X = record { s-alg-on = s-alg-on ; ρ-algebra-morphism = D-universal }
|
||||
where
|
||||
open Coequalizer (coeqs X) renaming (universal to coeq-universal)
|
||||
open IsCoequalizer (c-1 X) using () renaming (equality to D-equality; coequalize to D-coequalize; universal to D-universal; unique to D-unique)
|
||||
|
|
|
|||
305
src/Monad/Instance/Delay/Strong.lagda.md
Normal file
305
src/Monad/Instance/Delay/Strong.lagda.md
Normal file
|
|
@ -0,0 +1,305 @@
|
|||
<!--
|
||||
```agda
|
||||
open import Level
|
||||
|
||||
open import Data.Product using (_,_; proj₁; proj₂)
|
||||
open import Categories.Category
|
||||
open import Category.Instance.AmbientCategory
|
||||
open import Categories.Functor
|
||||
open import Categories.Functor.Coalgebra
|
||||
open import Monad.Instance.Delay
|
||||
open import Categories.Monad
|
||||
open import Categories.Monad.Strong
|
||||
open import Categories.Monad.Relative using () renaming (Monad to RMonad)
|
||||
open import Categories.NaturalTransformation
|
||||
open import Categories.Object.Terminal
|
||||
open import Categories.Monad.Relative using () renaming (Monad to RMonad)
|
||||
open import Categories.Category.Product renaming (Product to CProduct; _⁂_ to _×C_)
|
||||
```
|
||||
-->
|
||||
|
||||
```agda
|
||||
module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : DelayM ambient) where
|
||||
open Ambient ambient
|
||||
open HomReasoning
|
||||
open Equiv
|
||||
open MR C
|
||||
open M C
|
||||
open F-Coalgebra-Morphism renaming (f to u)
|
||||
```
|
||||
|
||||
# The Delay Monad is strong
|
||||
|
||||
```agda
|
||||
module _ where
|
||||
open DelayM D
|
||||
open Functor
|
||||
open RMonad kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
|
||||
open Monad monad using (η; μ)
|
||||
|
||||
-- TODO change 'coinduction' proofs, move the two proofs i.e. f ≈ ! and ! ≈ g to the where clause
|
||||
|
||||
strength : Strength monoidal monad
|
||||
strength = record
|
||||
{ strengthen = ntHelper (record
|
||||
{ η = τ
|
||||
; commute = commute' })
|
||||
; identityˡ = identityˡ' -- triangle
|
||||
; η-comm = begin -- η-τ
|
||||
τ _ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂) ⟩
|
||||
τ _ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullˡ (τ-helper _) ⟩
|
||||
(out⁻¹ ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullʳ (pullʳ dstr-law₁) ⟩
|
||||
out⁻¹ ∘ (idC +₁ τ _) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩
|
||||
out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
|
||||
now ∎
|
||||
; μ-η-comm = μ-η-comm' -- μ-τ
|
||||
; strength-assoc = strength-assoc' -- square
|
||||
}
|
||||
where
|
||||
out-law : ∀ {X Y} (f : X ⇒ Y) → out {Y} ∘ extend (now ∘ f) ≈ (f +₁ extend (now ∘ f)) ∘ out {X}
|
||||
out-law {X} {Y} f = begin
|
||||
out ∘ extend (now ∘ f) ≈⟨ extendlaw (now ∘ f) ⟩
|
||||
[ out ∘ now ∘ f , i₂ ∘ extend (now ∘ f) ] ∘ out ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩
|
||||
(f +₁ extend (now ∘ f)) ∘ out ∎
|
||||
|
||||
-- TODO add to agda-categories
|
||||
dstr-law₁ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₁) ≈ i₁
|
||||
dstr-law₁ = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ))
|
||||
dstr-law₂ : ∀ {A B C} → distributeˡ⁻¹ {A} {B} {C} ∘ (idC ⁂ i₂) ≈ i₂
|
||||
dstr-law₂ = (refl⟩∘⟨ (sym inject₂)) ○ (cancelˡ (IsIso.isoˡ isIsoˡ))
|
||||
|
||||
module _ (P : Category.Obj (CProduct C C)) where
|
||||
X = proj₁ P
|
||||
Y = proj₂ 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) }})
|
||||
|
||||
τ-helper : τ ∘ (idC ⁂ out⁻¹) ≈ out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹
|
||||
τ-helper = begin
|
||||
τ ∘ (idC ⁂ out⁻¹) ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩
|
||||
(out⁻¹ ∘ out) ∘ τ ∘ (idC ⁂ out⁻¹) ≈⟨ pullʳ (pullˡ τ-law) ⟩
|
||||
out⁻¹ ∘ ((idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ out⁻¹) ≈⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ assoc) ⟩
|
||||
out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ (idC ⁂ out⁻¹) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimʳ (⁂∘⁂ ○ (⁂-cong₂ identity² (_≅_.isoʳ out-≅)) ○ ((⟨⟩-cong₂ identityˡ identityˡ) ○ ⁂-η)))) ⟩
|
||||
out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∎
|
||||
|
||||
τ-now : τ ∘ (idC ⁂ now) ≈ now
|
||||
τ-now = begin
|
||||
τ ∘ (idC ⁂ now) ≈⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ (⁂-cong₂ identity² refl)) ⟩
|
||||
τ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullˡ τ-helper ⟩
|
||||
(out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₁) ≈⟨ pullʳ (pullʳ dstr-law₁) ⟩
|
||||
out⁻¹ ∘ (idC +₁ τ) ∘ i₁ ≈⟨ refl⟩∘⟨ +₁∘i₁ ⟩
|
||||
out⁻¹ ∘ i₁ ∘ idC ≈⟨ refl⟩∘⟨ identityʳ ⟩
|
||||
now ∎
|
||||
|
||||
▷∘τ : τ ∘ (idC ⁂ ▷) ≈ ▷ ∘ τ
|
||||
▷∘τ = begin
|
||||
τ ∘ (idC ⁂ ▷) ≈⟨ refl⟩∘⟨ (sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩
|
||||
τ ∘ (idC ⁂ out⁻¹) ∘ (idC ⁂ i₂) ≈⟨ pullˡ τ-helper ⟩
|
||||
(out⁻¹ ∘ (idC +₁ τ) ∘ distributeˡ⁻¹) ∘ (idC ⁂ i₂) ≈⟨ pullʳ (pullʳ dstr-law₂) ⟩
|
||||
out⁻¹ ∘ (idC +₁ τ) ∘ i₂ ≈⟨ refl⟩∘⟨ +₁∘i₂ ⟩
|
||||
out⁻¹ ∘ i₂ ∘ τ ≈⟨ sym-assoc ⟩
|
||||
▷ ∘ τ ∎
|
||||
|
||||
τ-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 }))
|
||||
|
||||
identityˡ' : ∀ {X : Obj} → extend (now ∘ π₂) ∘ τ (Terminal.⊤ terminal , X) ≈ π₂
|
||||
identityˡ' {X} = begin
|
||||
extend (now ∘ π₂) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras X) {A = record { A = Terminal.⊤ terminal × D₀ X ; α = (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }} (record { f = extend (now ∘ π₂) ∘ τ _ ; commutes = begin
|
||||
out ∘ extend (now ∘ π₂) ∘ τ _ ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (sym identityʳ)) ⟩
|
||||
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 +₁ τ _) ∘ (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ˡ +₁∘+₁ ⟩
|
||||
(idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ _) ∘ (idC ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (elimˡ identity²)) ⟩
|
||||
(idC +₁ extend (now ∘ π₂)) ∘ (π₂ +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ refl⟩∘⟨ ((+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl) ⟩
|
||||
(idC +₁ extend (now ∘ π₂)) ∘ (idC ∘ π₂ +₁ τ _ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullʳ (pullˡ +₁∘+₁) ⟩
|
||||
((idC +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ _)) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ (homomorphism (X +-)) ⟩∘⟨refl ⟩
|
||||
(idC +₁ extend (now ∘ π₂) ∘ τ _) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩
|
||||
u (Terminal.! (coalgebras X)) ≈⟨ Terminal.!-unique (coalgebras X) {A = record { A = Terminal.⊤ terminal × D₀ X ; α = (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }} (record { f = π₂ ; commutes = begin
|
||||
out ∘ π₂ ≈˘⟨ π₂∘⁂ ⟩
|
||||
π₂ ∘ (idC ⁂ out) ≈˘⟨ pullˡ distribute₂ ⟩
|
||||
(π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ (+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl ⟩
|
||||
(idC ∘ π₂ +₁ π₂ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈˘⟨ pullˡ +₁∘+₁ ⟩
|
||||
(idC +₁ π₂) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩
|
||||
π₂ ∎
|
||||
where
|
||||
diag₁ : (⟨ Terminal.! terminal , idC ⟩ +₁ idC) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈ distributeˡ⁻¹ {Terminal.⊤ terminal} {X} {D₀ X} ∘ (idC ⁂ out) ∘ idC
|
||||
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) ⟩
|
||||
distributeˡ⁻¹ ∘ (idC ⁂ out) ∘ idC ∎
|
||||
diag₂ = τ-law
|
||||
diag₃ : out {X} ∘ extend (now ∘ π₂ {A = Terminal.⊤ terminal} {B = X}) ≈ (π₂ +₁ extend (now ∘ π₂)) ∘ out
|
||||
diag₃ = out-law π₂
|
||||
-- TODO add to agda-categories
|
||||
distribute₂ : ∀ {A B C} → (π₂ +₁ π₂) ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₂
|
||||
distribute₂ = sym (begin
|
||||
π₂ ≈⟨ introʳ (IsIso.isoʳ isIsoˡ) ⟩
|
||||
π₂ ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ pullˡ ∘[] ⟩
|
||||
[ π₂ ∘ ((idC ⁂ i₁)) , π₂ ∘ (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ π₂∘⁂ π₂∘⁂) ⟩∘⟨refl ⟩
|
||||
(π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∎)
|
||||
|
||||
μ-η-comm' : ∀ {X Y} → extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈ τ (X , Y) ∘ (idC ⁂ extend idC)
|
||||
μ-η-comm' {X} {Y} = begin
|
||||
extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y)) (record { f = extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ; commutes = begin
|
||||
out ∘ extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _ ≈⟨ refl⟩∘⟨ (pullˡ id*∘Dτ) ⟩
|
||||
out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ square ⟩
|
||||
[ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ sym-assoc ○ (assoc ○ tri) ⟩∘⟨refl ⟩
|
||||
((idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩
|
||||
(idC +₁ (extend (τ _) ∘ τ _)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ refl (sym (pullˡ id*∘Dτ))) ⟩∘⟨refl ⟩
|
||||
(idC +₁ (extend idC ∘ extend (now ∘ τ (X , Y)) ∘ τ _)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩
|
||||
u (Terminal.! (coalgebras (X × Y)) {A = record { A = X × D₀ (D₀ Y) ; α = [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }}) ≈⟨ Terminal.!-unique (coalgebras (X × Y)) (record { f = τ _ ∘ (idC ⁂ extend idC) ; commutes = begin
|
||||
out ∘ τ _ ∘ (idC ⁂ extend idC) ≈⟨ pullˡ (τ-law (X , Y)) ⟩
|
||||
((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ extend idC) ≈⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)) ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out ∘ extend idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (extendlaw idC) ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out ∘ idC , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ refl (([]-cong₂ identityʳ refl) ⟩∘⟨refl) ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ] ∘ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ sym (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ out) ≈⟨ sym-assoc ○ pullˡ (assoc ○ tri₂) ⟩
|
||||
((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc ○ refl⟩∘⟨ assoc ⟩
|
||||
(idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩
|
||||
τ _ ∘ (idC ⁂ extend idC) ∎
|
||||
where
|
||||
-- diagram: https://q.uiver.app/#q=WzAsNyxbMCwwLCJYXFx0aW1lcyBERFkiXSxbMiwwLCJEKFhcXHRpbWVzIERZKSJdLFs0LDAsIkREKFhcXHRpbWVzIFkpIl0sWzAsMiwiWFxcdGltZXMgKERZK0REWSkiXSxbMiwyLCJYXFx0aW1lcyBEWSsgWFxcdGltZXMgRERZIl0sWzQsMiwiWFxcdGltZXMgWSsgREQoWFxcdGltZXMgWSkiXSxbMCw0LCJYXFx0aW1lcyBZKyBYXFx0aW1lcyBERFkiXSxbMCwzLCJpZFxcdGltZXMgb3V0IiwyXSxbMCwxLCJcXHRhdSJdLFsxLDIsIlxcdGF1XioiXSxbMyw0LCIoaWQrXFx0YXUpZGlzdCJdLFs0LDUsIltvdXRcXHRhdSxpbnJcXHRhdV4qXSJdLFsyLDUsIm91dCJdLFsxLDRdLFs2LDUsImlkK1xcdGF1XipcXHRhdSIsMl0sWzMsNiwiWyhpZCArIGlkXFx0aW1lcyBub3cpZGlzdCAoaWRcXHRpbWVzIG91dCksaW5yXWRpc3QiLDJdXQ==
|
||||
square : out ∘ extend (τ (X , Y)) ∘ τ _ ≈ [ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)
|
||||
square = begin
|
||||
out ∘ extend (τ (X , Y)) ∘ τ _ ≈⟨ pullˡ (extendlaw (τ (X , Y))) ⟩
|
||||
([ out ∘ τ (X , Y) , i₂ ∘ extend (τ (X , Y)) ] ∘ out) ∘ τ _ ≈⟨ pullʳ (τ-law _) ⟩
|
||||
[ out ∘ τ _ , i₂ ∘ extend (τ _) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎
|
||||
tri : [ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈ (idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹
|
||||
tri = begin
|
||||
[ out ∘ τ _ , i₂ ∘ extend (τ (X , Y)) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ≈⟨ pullˡ []∘+₁ ⟩
|
||||
[ (out ∘ τ _) ∘ idC , (i₂ ∘ extend (τ (X , Y))) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ (identityʳ ○ τ-law (X , Y)) assoc) ⟩∘⟨refl ⟩
|
||||
[ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ (X , Y)) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ refl k-identityʳ) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩
|
||||
[ (idC +₁ extend (τ _) ∘ now) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ ((+₁-cong₂ identity² (pullʳ (τ-now (X , D₀ Y)))) ⟩∘⟨refl) refl) ⟩∘⟨refl) ⟩
|
||||
[ (idC ∘ idC +₁ (extend (τ _) ∘ τ _) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ extend (τ _) ∘ τ _ ] ∘ distributeˡ⁻¹ ≈⟨ sym (([]-cong₂ (pullˡ +₁∘+₁) +₁∘i₂) ⟩∘⟨refl) ⟩
|
||||
[ (idC +₁ extend (τ _) ∘ τ _) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ extend (τ _) ∘ τ _) ∘ i₂ ] ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ ∘[]) ⟩
|
||||
(idC +₁ extend (τ _) ∘ τ _) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∎
|
||||
id*∘Dτ : extend idC ∘ extend (now ∘ τ _) ≈ extend (τ _)
|
||||
id*∘Dτ = begin
|
||||
extend idC ∘ extend (now ∘ τ _) ≈⟨ sym k-assoc ⟩
|
||||
extend (extend idC ∘ now ∘ τ _) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩
|
||||
extend (idC ∘ τ _) ≈⟨ extend-≈ identityˡ ⟩
|
||||
extend (τ _) ∎
|
||||
tri₂' : (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ
|
||||
tri₂' = begin
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ [ (idC ⁂ i₁) , (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ∘[]) ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₁) , (idC ⁂ [ out , i₂ ∘ extend idC ]) ∘ (idC ⁂ i₂) ] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []-cong₂ ⁂∘⁂ ⁂∘⁂ ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ (idC ∘ idC ⁂ [ out , i₂ ∘ extend idC ] ∘ i₁) , (idC ∘ idC ⁂ [ out , i₂ ∘ extend idC ] ∘ i₂) ] ≈⟨ refl⟩∘⟨ refl⟩∘⟨ []-cong₂ (⁂-cong₂ identity² inject₁) (⁂-cong₂ identity² inject₂) ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ [ idC ⁂ out , idC ⁂ i₂ ∘ extend idC ] ≈⟨ refl⟩∘⟨ ∘[] ⟩
|
||||
(idC +₁ τ _) ∘ [ distributeˡ⁻¹ ∘ (idC ⁂ out) , distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ ∘[] ⟩
|
||||
[ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂ ∘ extend idC) ] ≈⟨ sym ([]-cong₂ refl (pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩
|
||||
[ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ i₂)) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl ((refl⟩∘⟨ dstr-law₂) ⟩∘⟨refl) ⟩
|
||||
[ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , ((idC +₁ τ _) ∘ i₂) ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ refl (pushˡ +₁∘i₂) ⟩
|
||||
[ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((+₁-cong₂ refl (introʳ (⟨⟩-unique id-comm (id-comm ○ (sym k-identityʳ) ⟩∘⟨refl)))) ⟩∘⟨refl) refl ⟩
|
||||
[ (idC +₁ τ _ ∘ (idC ⁂ extend idC ∘ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ []-cong₂ ((sym (+₁-cong₂ refl (refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl)))) ⟩∘⟨refl) refl ⟩
|
||||
[ (idC +₁ τ _ ∘ (idC ⁂ extend idC) ∘ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ∘ τ _ ∘ (idC ⁂ extend idC) ] ≈⟨ sym ([]-cong₂ (pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² assoc)) +₁∘i₂) ⟩
|
||||
[ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ i₂ ] ≈⟨ sym ∘[] ⟩
|
||||
(idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ≈⟨ sym (refl⟩∘⟨ (elimʳ (IsIso.isoˡ isIsoˡ))) ⟩
|
||||
(idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹ ∘ distributeˡ ∎
|
||||
tri₂ : (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]) ≈ (idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹
|
||||
tri₂ = iso-epi-from
|
||||
(record { from = distributeˡ ; to = distributeˡ⁻¹ ; iso = IsIso.iso isIsoˡ })
|
||||
((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ [ out , i₂ ∘ extend idC ]))
|
||||
((idC +₁ τ _ ∘ (idC ⁂ extend idC)) ∘ [ (idC +₁ (idC ⁂ now)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) , i₂ ] ∘ distributeˡ⁻¹)
|
||||
(assoc ○ refl⟩∘⟨ assoc ○ tri₂' ○ sym-assoc ○ sym-assoc ○ assoc ⟩∘⟨refl)
|
||||
|
||||
strength-assoc' : ∀ {X Y Z} → extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ ((X × Y), Z) ≈ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩
|
||||
strength-assoc' {X} {Y} {Z} = begin
|
||||
extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras (X × Y × Z)) (record { f = extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ; commutes = begin
|
||||
out ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _ ≈⟨ pullˡ (extendlaw (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ⟩
|
||||
([ out ∘ now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , i₂ ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ] ∘ out) ∘ τ _ ≈⟨ pullʳ (τ-law (X × Y , Z)) ⟩
|
||||
[ out ∘ now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , i₂ ∘ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ ([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl ⟩
|
||||
(⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩
|
||||
(⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ idC +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ id-comm (sym identityʳ)) ⟩∘⟨refl ⟩
|
||||
(idC ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ (extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym (pullˡ +₁∘+₁) ⟩
|
||||
(idC +₁ extend (now ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ τ _) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ })) ⟩
|
||||
u (Terminal.! (coalgebras (X × Y × Z)) {A = record { A = (X × Y) × D₀ Z ; α = (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }}) ≈⟨ Terminal.!-unique (coalgebras (X × Y × Z)) (record { f = τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ; commutes = begin
|
||||
out ∘ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullˡ (τ-law (X , Y × Z)) ⟩
|
||||
((idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullʳ (pullˡ (pullʳ ⁂∘⁂)) ⟩
|
||||
(idC +₁ τ _) ∘ (distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ out ∘ τ _)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ assoc ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ out ∘ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈˘⟨ refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ identityʳ (assoc ○ sym (τ-law (Y , Z)))) ⟩∘⟨refl) ⟩
|
||||
(idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ ((idC ∘ idC) ∘ idC ⁂ ((idC +₁ τ _) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ sym (refl⟩∘⟨ (pullʳ (pullˡ ⁂∘⁂ ○ pullˡ ⁂∘⁂))) ⟩
|
||||
(idC +₁ τ _) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ _))) ∘ (idC ⁂ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ (refl⟩∘⟨ helper₁)) ⟩
|
||||
(idC +₁ τ _) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ _))) ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (helper₂ ⟩∘⟨refl) ⟩
|
||||
(idC +₁ τ _) ∘ ((idC +₁ (idC ⁂ τ (Y , Z))) ∘ distributeˡ⁻¹) ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (assoc ○ refl⟩∘⟨ sym assoc²') ⟩
|
||||
(idC +₁ τ _) ∘ (idC +₁ (idC ⁂ τ (Y , Z))) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ out) ≈⟨ pullˡ (+₁∘+₁ ○ +₁-cong₂ identity² refl) ⟩
|
||||
(idC +₁ τ _ ∘ (idC ⁂ τ (Y , Z))) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ (helper₃ ⟩∘⟨refl) ⟩
|
||||
(idC +₁ τ _ ∘ (idC ⁂ τ (Y , Z))) ∘ ((⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹) ∘ (idC ⁂ out) ≈⟨ assoc²'' ⟩
|
||||
((idC +₁ τ _ ∘ (idC ⁂ τ _)) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym ((+₁-cong₂ refl (identityʳ ○ sym-assoc) ○ sym +₁∘+₁) ⟩∘⟨refl) ⟩
|
||||
(idC ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ (τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ sym (pullˡ +₁∘+₁) ⟩
|
||||
(idC +₁ τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ∎ }) ⟩
|
||||
τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎
|
||||
where
|
||||
helper₁ : (idC ⁂ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC {X × Y} ⁂ out {Z})
|
||||
helper₁ = begin
|
||||
(idC ⁂ (idC ⁂ out)) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ ⁂∘⟨⟩ ⟩
|
||||
⟨ idC ∘ π₁ ∘ π₁ , (idC ⁂ out) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ identityˡ ⁂∘⟨⟩ ⟩
|
||||
⟨ π₁ ∘ π₁ , ⟨ idC ∘ π₂ ∘ π₁ , out ∘ π₂ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ refl (⟨⟩-cong₂ identityˡ refl) ⟩
|
||||
⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , out ∘ π₂ ⟩ ⟩ ≈⟨ sym (⟨⟩-cong₂ refl (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) refl)) ⟩
|
||||
⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ idC ∘ π₁ , out ∘ π₂ ⟩ ⟩ ≈⟨ sym (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)) ⟩
|
||||
⟨ π₁ ∘ idC ∘ π₁ , ⟨ (π₂ ∘ π₁) ∘ (idC {X × Y} ⁂ out {Z}) , π₂ ∘ (idC {X × Y} ⁂ out {Z}) ⟩ ⟩ ≈⟨ sym (⟨⟩-cong₂ (pullʳ project₁) ⟨⟩∘) ⟩
|
||||
⟨ (π₁ ∘ π₁) ∘ (idC {X × Y} ⁂ out {Z}) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC {X × Y} ⁂ out {Z}) ⟩ ≈⟨ sym ⟨⟩∘ ⟩
|
||||
⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC {X × Y} ⁂ out {Z}) ∎
|
||||
helper₂ : distributeˡ⁻¹ ∘ (idC ⁂ (idC +₁ τ _)) ≈ (idC +₁ (idC ⁂ τ (Y , Z))) ∘ distributeˡ⁻¹
|
||||
helper₂ = sym (distribute₁ idC idC (τ _)) ○ (+₁-cong₂ (⟨⟩-unique id-comm id-comm) refl) ⟩∘⟨refl
|
||||
helper₃ : distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹
|
||||
helper₃ = sym (begin
|
||||
(⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹ ≈⟨ introˡ (IsIso.isoˡ isIsoˡ) ⟩
|
||||
(distributeˡ⁻¹ ∘ distributeˡ) ∘ (⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ +₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ⁻¹ ≈⟨ pullʳ (pullˡ []∘+₁) ⟩
|
||||
distributeˡ⁻¹ ∘ [ (idC ⁂ i₁) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , (idC ⁂ i₂) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ (([]-cong₂ ⁂∘⟨⟩ ⁂∘⟨⟩) ⟩∘⟨refl) ⟩
|
||||
distributeˡ⁻¹ ∘ [ ⟨ idC ∘ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , ⟨ idC ∘ π₁ ∘ π₁ , i₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ identityˡ (pushˡ (sym dstr-law₁))) (⟨⟩-cong₂ identityˡ ((pushˡ (sym dstr-law₂)))) ⟩∘⟨refl ⟩
|
||||
distributeˡ⁻¹ ∘ [ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₁) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₂) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ refl (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ ○ sym identityˡ) refl ○ sym ⁂∘⟨⟩))) (⟨⟩-cong₂ refl (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ ○ sym identityˡ) refl ○ sym ⁂∘⟨⟩))) ⟩∘⟨refl) ⟩
|
||||
distributeˡ⁻¹ ∘ [ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ , ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ (identityˡ ○ refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂))) (⟨⟩-cong₂ (identityˡ ○ refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂))) ⟩∘⟨refl) ⟩
|
||||
distributeˡ⁻¹ ∘ [ ⟨ idC ∘ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₁) , π₂ ∘ (idC ⁂ i₁) ⟩ ⟩ , ⟨ idC ∘ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₂) , π₂ ∘ (idC ⁂ i₂) ⟩ ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ (⟨⟩-cong₂ (pullʳ (pullʳ π₁∘⁂)) (pullʳ ⟨⟩∘)) (⟨⟩-cong₂ (pullʳ (pullʳ π₁∘⁂)) (pullʳ ⟨⟩∘)) ⟩∘⟨refl) ⟩
|
||||
distributeˡ⁻¹ ∘ [ ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ i₁) , (distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ i₁) ⟩ , ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ i₂) , (distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ i₂) ⟩ ] ∘ distributeˡ⁻¹ ≈⟨ sym (refl⟩∘⟨ []-cong₂ ⟨⟩∘ ⟨⟩∘ ⟩∘⟨refl) ⟩
|
||||
distributeˡ⁻¹ ∘ [ (⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ i₁)) , (⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ (idC ⁂ i₂)) ] ∘ distributeˡ⁻¹ ≈˘⟨ pullʳ (pullˡ ∘[]) ⟩
|
||||
(distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ sym (introʳ (IsIso.isoʳ isIsoˡ)) ⟩
|
||||
distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ sym (refl⟩∘⟨ ⁂∘⟨⟩) ⟩
|
||||
distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎)
|
||||
-- {- ⁂ ⊤ ○
|
||||
-- Diagram for identityˡ':
|
||||
-- https://q.uiver.app/#q=WzAsOSxbMCwyLCIxIFxcdGltZXMgREIiXSxbMiwyLCIxIFxcdGltZXMgKEIgKyBEQikiXSxbNiwyLCIxIFxcdGltZXMgQiArIDEgXFx0aW1lcyBEQiJdLFswLDQsIkQoMSBcXHRpbWVzIEIpIl0sWzYsNCwiKDEgXFx0aW1lcyBCKSArIEQoMSBcXHRpbWVzIEIpIl0sWzAsNiwiREIiXSxbNiw2LCJCICsgREIiXSxbMCwwLCIxIFxcdGltZXMgREIiXSxbNiwwLCJCICsgMSBcXHRpbWVzIERCIl0sWzAsMSwiaWQgXFx0aW1lcyBvdXQiXSxbMSwyLCJkaXN0cmliXnstMX0iXSxbMCwzLCJcXHRhdSIsMl0sWzUsNiwib3V0IiwyXSxbMyw0LCJvdXQiLDJdLFsyLDQsImlkICsgXFx0YXUiXSxbMyw1LCJEIFxccGlfMiJdLFs0LDYsIlxccGlfMiArIEQgXFxwaV8yIl0sWzcsOCwiKFxccGlfMiArIGlkKSBcXGNpcmMgZGlzdHJpYl57LTF9IFxcY2lyYyAoaWQgXFx0aW1lcyBvdXQpIl0sWzcsMCwiaWQiXSxbOCwyLCJcXGxhbmdsZSAhICwgaWQgXFxyYW5nbGUgKyBpZCJdXQ==
|
||||
-- -}
|
||||
commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂)
|
||||
→ τ P₂ ∘ ((proj₁ fg) ⁂ extend (now ∘ (proj₂ fg))) ≈ extend (now ∘ ((proj₁ fg) ⁂ (proj₂ 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) }
|
||||
|
||||
strongMonad : StrongMonad monoidal
|
||||
strongMonad = record { M = monad ; strength = strength }
|
||||
```
|
||||
Loading…
Reference in a new issue