mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Compare commits
No commits in common. "bf4af5ad9c9ad1c7ab3151b3fa2bfc736604d964" and "a71045161a1250ab05d237aba140db94e8c9b0fa" have entirely different histories.
bf4af5ad9c
...
a71045161a
6 changed files with 62 additions and 343 deletions
|
|
@ -5,11 +5,6 @@ open import Level
|
|||
open import Category.Instance.AmbientCategory
|
||||
open import Categories.Functor
|
||||
open import Categories.Monad.Relative renaming (Monad to RMonad)
|
||||
open import Categories.Object.Initial
|
||||
open import Categories.Object.Terminal
|
||||
open import Categories.Object.NaturalNumbers.Properties.F-Algebras
|
||||
open import Categories.Functor.Algebra
|
||||
open import Categories.Functor.Coalgebra
|
||||
```
|
||||
-->
|
||||
|
||||
|
|
@ -29,65 +24,12 @@ module Algebra.Elgot.Properties {o ℓ e} (ambient : Ambient o ℓ e) where
|
|||
module _ {D : DelayM} (algebra : Guarded-Elgot-Algebra (DelayM.functor D)) where
|
||||
open DelayM D
|
||||
open Functor functor renaming (F₁ to D₁)
|
||||
open RMonad kleisli using (extend)
|
||||
open RMonad kleisli
|
||||
open Guarded-Elgot-Algebra algebra
|
||||
open MR C
|
||||
open M C
|
||||
|
||||
commutes : α ∘ extend ι ≈ α ∘ (D₁ π₁)
|
||||
commutes = {! !}
|
||||
where
|
||||
α∘ι : α ∘ ι ≈ π₁
|
||||
α∘ι = begin
|
||||
α ∘ ι ≈⟨ sym (IsInitial.!-unique isInitial (record { f = α ∘ ι ; commutes = begin
|
||||
(α ∘ ι) ∘ [ ⟨ idC , z ∘ _ ⟩ , idC ⁂ s ] ≈⟨ ∘[] ⟩
|
||||
[ (α ∘ ι) ∘ ⟨ idC , z ∘ _ ⟩ , (α ∘ ι) ∘ (idC ⁂ s) ] ≈⟨ []-cong₂ helper₁ (pullʳ helper₂) ⟩
|
||||
[ idC , α ∘ ι ] ≈˘⟨ {! !} ⟩
|
||||
{! !} ≈˘⟨ {! !} ⟩
|
||||
[ idC , idC ] ∘ [ i₁ , i₂ ∘ α ∘ ι ] ∎ })) ⟩
|
||||
F-Algebra-Morphism.f (IsInitial.! isInitial) ≈⟨ IsInitial.!-unique isInitial (record { f = π₁ ; commutes = begin
|
||||
π₁ ∘ [ ⟨ idC , z ∘ _ ⟩ , idC ⁂ s ] ≈⟨ ∘[] ⟩
|
||||
[ π₁ ∘ ⟨ idC , z ∘ _ ⟩ , π₁ ∘ (idC ⁂ s) ] ≈⟨ []-cong₂ project₁ π₁∘⁂ ⟩
|
||||
[ idC , idC ∘ π₁ ] ≈˘⟨ []-cong₂ inject₁ (pullˡ inject₂) ⟩
|
||||
[ [ idC , idC ] ∘ i₁ , [ idC , idC ] ∘ i₂ ∘ π₁ ] ≈˘⟨ ∘[] ⟩
|
||||
[ idC , idC ] ∘ [ i₁ , i₂ ∘ π₁ ] ∎ }) ⟩
|
||||
π₁ ∎
|
||||
where
|
||||
isInitial = PNNO⇒Initial₂ cartesianCategory coproducts ℕ A
|
||||
helper₁ = begin
|
||||
(α ∘ ι) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ pullʳ (sym (Terminal.!-unique (coalgebras A) (record { f = ι ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ; commutes = begin
|
||||
out ∘ ι ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈⟨ pullˡ ι-commutes ⟩
|
||||
((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩ ≈˘⟨ refl⟩∘⟨ inject₁ ⟩
|
||||
((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ _≅_.to nno-iso ∘ i₁ ≈⟨ pullʳ (cancelˡ (_≅_.isoʳ nno-iso)) ⟩
|
||||
(idC +₁ ι) ∘ i₁ ≈⟨ +₁∘i₁ ○ identityʳ ⟩
|
||||
i₁ ≈˘⟨ +₁∘i₁ ○ identityʳ ⟩
|
||||
(idC +₁ ι ∘ ⟨ idC , z ∘ Terminal.! terminal ⟩) ∘ i₁ ∎ }))) ⟩
|
||||
α ∘ F-Coalgebra-Morphism.f (Terminal.! (coalgebras A)) ≈⟨ refl⟩∘⟨ (Terminal.!-unique (coalgebras A) (record { f = now ; commutes = begin
|
||||
out ∘ now ≈⟨ unitlaw ⟩
|
||||
i₁ ≈˘⟨ +₁∘i₁ ○ identityʳ ⟩
|
||||
(idC +₁ now) ∘ i₁ ∎ })) ⟩
|
||||
α ∘ now ≈⟨ {! !} ⟩ -- TODO elgot⇒search
|
||||
idC ∎
|
||||
helper₂ = begin
|
||||
ι ∘ (idC ⁂ s) ≈⟨ sym (Terminal.!-unique (coalgebras A) (record { f = ι ∘ (idC ⁂ s) ; commutes = begin
|
||||
out ∘ ι ∘ (idC ⁂ s) ≈⟨ pullˡ ι-commutes ⟩
|
||||
((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ (idC ⁂ s) ≈⟨ {! !} ⟩
|
||||
((idC +₁ ι) ∘ _≅_.from nno-iso) ∘ _≅_.to nno-iso ∘ i₂ ≈⟨ {! !} ⟩
|
||||
(idC +₁ ι) ∘ i₂ ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
((idC +₁ ι) ∘ (idC +₁ (idC ⁂ s))) ∘ _≅_.from nno-iso ≈⟨ {! !} ⟩
|
||||
(idC +₁ ι ∘ (idC ⁂ s)) ∘ _≅_.from nno-iso ∎ })) ⟩
|
||||
-- TODO remove last part, iota is the final morphism...
|
||||
F-Coalgebra-Morphism.f (Terminal.! (coalgebras A)) ≈⟨ Terminal.!-unique (coalgebras A) (record { f = ι ; commutes = begin
|
||||
out ∘ ι ≈⟨ ι-commutes ⟩
|
||||
(idC +₁ ι) ∘ _≅_.from nno-iso ∎ }) ⟩
|
||||
ι ∎
|
||||
```
|
||||
|
||||
- For every X, a final coalgebra Y → X + H Y is a free H-guarded algebra over X.
|
||||
|
||||
```agda
|
||||
-- final-to-guarded : ∀ {A} → ?η
|
||||
α∘ι = {! !}
|
||||
```
|
||||
|
|
@ -14,9 +14,6 @@ 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.Monad
|
||||
open import Categories.Monad.Construction.Kleisli
|
||||
open import Categories.Monad.Relative renaming (Monad to RMonad)
|
||||
open import Categories.Category.Cocartesian using (Cocartesian)
|
||||
open import Categories.Object.NaturalNumbers.Parametrized using (ParametrizedNNO)
|
||||
open import Categories.Object.Exponential using (Exponential)
|
||||
|
|
@ -88,6 +85,7 @@ module Category.Instance.AmbientCategory where
|
|||
[ (idC ⁂ i₁) ∘ swap , (idC ⁂ i₂) ∘ swap ] ∘ distributeʳ⁻¹ ≈⟨ sym (pullˡ []∘+₁) ⟩
|
||||
distributeˡ ∘ (swap +₁ swap) ∘ distributeʳ⁻¹ ∎)
|
||||
|
||||
|
||||
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₂
|
||||
|
|
@ -96,12 +94,6 @@ module Category.Instance.AmbientCategory where
|
|||
dstr-law₃ = (refl⟩∘⟨ (sym inject₁)) ○ (cancelˡ (IsIso.isoˡ isIsoʳ))
|
||||
dstr-law₄ : ∀ {A B C} → distributeʳ⁻¹ {A} {B} {C} ∘ (i₂ ⁂ idC) ≈ i₂
|
||||
dstr-law₄ = (refl⟩∘⟨ (sym inject₂)) ○ (cancelˡ (IsIso.isoˡ isIsoʳ))
|
||||
dstr-law₅ : ∀ {A B C} → (π₂ +₁ π₂) ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₂
|
||||
dstr-law₅ = Iso⇒Epi C (IsIso.iso isIsoˡ) ((π₂ +₁ π₂) ∘ distributeˡ⁻¹) π₂ (begin
|
||||
(((π₂ +₁ π₂) ∘ distributeˡ⁻¹) ∘ distributeˡ) ≈⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩
|
||||
(π₂ +₁ π₂) ≈˘⟨ []-cong₂ project₂ project₂ ⟩
|
||||
[ π₂ ∘ _ , π₂ ∘ _ ] ≈˘⟨ ∘[] ⟩
|
||||
π₂ ∘ distributeˡ ∎)
|
||||
distribute₂ : ∀ {A B C} → (π₂ +₁ π₂) ∘ distributeˡ⁻¹ {A} {B} {C} ≈ π₂
|
||||
distribute₂ = sym (begin
|
||||
π₂ ≈⟨ introʳ (IsIso.isoʳ isIsoˡ) ⟩
|
||||
|
|
@ -109,22 +101,6 @@ module Category.Instance.AmbientCategory where
|
|||
[ π₂ ∘ ((idC ⁂ i₁)) , π₂ ∘ (idC ⁂ i₂) ] ∘ distributeˡ⁻¹ ≈⟨ ([]-cong₂ π₂∘⁂ π₂∘⁂) ⟩∘⟨refl ⟩
|
||||
(π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∎)
|
||||
|
||||
distributeˡ⁻¹-assoc : ∀ {A B C D : Obj} → distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc ≈ (_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹ {A × B} {C} {D}
|
||||
distributeˡ⁻¹-assoc {A} {B} {U} {D} = Iso⇒Epi C (IsIso.iso isIsoˡ) (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ((_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹) (begin
|
||||
(distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ∘ [ idC ⁂ i₁ , idC ⁂ i₂ ] ≈⟨ ∘[] ⟩
|
||||
[ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ∘ (idC ⁂ i₁) , (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ _≅_.to ×-assoc) ∘ (idC ⁂ i₂) ] ≈⟨ []-cong₂ (pullʳ (pullʳ ⟨⟩∘)) (pullʳ (pullʳ ⟨⟩∘)) ⟩
|
||||
[ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₁) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₁) ⟩ , distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₂) , ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₂) ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ ⁂∘⟨⟩) (refl⟩∘⟨ ⁂∘⟨⟩) ⟩
|
||||
[ distributeˡ⁻¹ ∘ ⟨ idC ∘ (π₁ ∘ π₁) ∘ (idC ⁂ i₁) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₁) ⟩ , distributeˡ⁻¹ ∘ ⟨ idC ∘ (π₁ ∘ π₁) ∘ (idC ⁂ i₂) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₂) ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ refl)) (refl⟩∘⟨ (⟨⟩-cong₂ identityˡ refl)) ⟩
|
||||
[ distributeˡ⁻¹ ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₁) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₁) ⟩ , distributeˡ⁻¹ ∘ ⟨ (π₁ ∘ π₁) ∘ (idC ⁂ i₂) , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ∘ (idC ⁂ i₂) ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) (refl⟩∘⟨ ⟨⟩∘))) (refl⟩∘⟨ ⟨⟩-cong₂ (pullʳ π₁∘⁂) (refl⟩∘⟨ ⟨⟩∘)) ⟩
|
||||
[ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₁) , π₂ ∘ (idC ⁂ i₁) ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ idC ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ i₂) , π₂ ∘ (idC ⁂ i₂) ⟩ ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)))) (refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)))) ⟩
|
||||
[ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ π₂ ∘ idC ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ ⟨⟩-cong₂ ((refl⟩∘⟨ identityˡ) ○ sym identityˡ) refl)) (refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ ⟨⟩-cong₂ ((refl⟩∘⟨ identityˡ) ○ sym identityˡ) refl)) ⟩
|
||||
[ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ idC ∘ π₂ ∘ π₁ , i₁ ∘ π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ ⟨ idC ∘ π₂ ∘ π₁ , i₂ ∘ π₂ ⟩ ⟩ ] ≈˘⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ ⁂∘⟨⟩))) (refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ ⁂∘⟨⟩))) ⟩
|
||||
[ distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₁) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ π₁ ∘ π₁ , distributeˡ⁻¹ ∘ (idC ⁂ i₂) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ≈⟨ []-cong₂ (refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (pullˡ dstr-law₁))) (refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (pullˡ dstr-law₂))) ⟩
|
||||
[ distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , i₁ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ ⟨ idC ∘ π₁ ∘ π₁ , i₂ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ≈˘⟨ []-cong₂ (refl⟩∘⟨ ⁂∘⟨⟩) (refl⟩∘⟨ ⁂∘⟨⟩) ⟩
|
||||
[ distributeˡ⁻¹ ∘ (idC ⁂ i₁) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ , distributeˡ⁻¹ ∘ (idC ⁂ i₂) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ] ≈⟨ []-cong₂ (pullˡ dstr-law₁) (pullˡ dstr-law₂) ⟩
|
||||
(_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ≈˘⟨ cancelʳ (IsIso.isoˡ isIsoˡ) ⟩
|
||||
((_≅_.to ×-assoc +₁ _≅_.to ×-assoc) ∘ distributeˡ⁻¹) ∘ distributeˡ ∎)
|
||||
|
||||
module M = M'
|
||||
module MR = MR'
|
||||
|
||||
|
|
@ -151,8 +127,18 @@ module Category.Instance.AmbientCategory where
|
|||
[ ((g +₁ h) ⁂ f) ∘ (i₁ ⁂ idC) , ((g +₁ h) ⁂ f) ∘ (i₂ ⁂ idC) ] ≈˘⟨ ∘[] ⟩
|
||||
(((g +₁ h) ⁂ f) ∘ distributeʳ) ≈˘⟨ cancelˡ (IsIso.isoʳ isIsoʳ) ⟩∘⟨refl ⟩
|
||||
(distributeʳ ∘ distributeʳ⁻¹ ∘ ((g +₁ h) ⁂ f)) ∘ distributeʳ ∎))
|
||||
dstldstr : ∀ {X Y U V} → (distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹ ≈ [ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ (distributeˡ⁻¹ {X + Y} {U} {V})
|
||||
dstldstr = Iso⇒Epi C (IsIso.iso isIsoˡ) ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) (sym (begin
|
||||
(([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹) ∘ distributeˡ) ≈⟨ pullʳ (cancelʳ (IsIso.isoˡ isIsoˡ)) ⟩
|
||||
([ i₁ +₁ i₁ , i₂ +₁ i₂ ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹)) ≈⟨ []∘+₁ ⟩
|
||||
[ (i₁ +₁ i₁) ∘ distributeʳ⁻¹ , (i₂ +₁ i₂) ∘ distributeʳ⁻¹ ] ≈⟨ {! !} ⟩
|
||||
{! !} ≈˘⟨ {! !} ⟩
|
||||
{! !} ≈˘⟨ {! !} ⟩
|
||||
{! !} ≈˘⟨ {! !} ⟩
|
||||
{! !} ≈˘⟨ {! !} ⟩
|
||||
[ ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (idC ⁂ i₁) , ((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ (idC ⁂ i₂) ] ≈˘⟨ ∘[] ⟩
|
||||
(((distributeˡ⁻¹ +₁ distributeˡ⁻¹) ∘ distributeʳ⁻¹) ∘ distributeˡ) ∎))
|
||||
|
||||
-- TODO replace with use of Iso⇒Epi etc.
|
||||
iso-epi-from : ∀ {X Y} → (iso : X ≅ Y) → Epi (_≅_.from iso)
|
||||
iso-epi-from iso = λ f g eq → begin
|
||||
f ≈⟨ introʳ (_≅_.isoʳ iso) ⟩
|
||||
|
|
@ -165,29 +151,4 @@ module Category.Instance.AmbientCategory where
|
|||
(f ∘ M'._≅_.to iso ∘ M'._≅_.from iso) ≈⟨ pullˡ eq ⟩
|
||||
((g ∘ M'._≅_.to iso) ∘ M'._≅_.from iso) ≈⟨ cancelʳ (_≅_.isoˡ iso) ⟩
|
||||
g ∎
|
||||
|
||||
-- TODO should be in agda-categories
|
||||
Kleisli⇒Monad⇒Kleisli : ∀ (K : KleisliTriple C) {X Y} (f : X ⇒ RMonad.F₀ K Y) → RMonad.extend (Monad⇒Kleisli C (Kleisli⇒Monad C K)) f ≈ RMonad.extend K f
|
||||
Kleisli⇒Monad⇒Kleisli K f = begin
|
||||
extend idC ∘ extend (unit ∘ f) ≈⟨ sym kleisli.assoc ⟩
|
||||
extend (extend idC ∘ unit ∘ f) ≈⟨ extend-≈ (pullˡ kleisli.identityʳ) ⟩
|
||||
extend (idC ∘ f) ≈⟨ extend-≈ (identityˡ) ⟩
|
||||
extend f ∎
|
||||
where
|
||||
module kleisli = RMonad K
|
||||
open kleisli using (unit; extend; extend-≈)
|
||||
Monad⇒Kleisli⇒Monad : ∀ (M : Monad C) {X Y} (f : X ⇒ Monad.F.₀ M Y) → Monad.F.₁ (Kleisli⇒Monad C (Monad⇒Kleisli C M)) f ≈ Monad.F.₁ M f
|
||||
Monad⇒Kleisli⇒Monad M f = begin
|
||||
μ.η _ ∘ F.₁ (η.η _ ∘ f) ≈⟨ refl⟩∘⟨ F.homomorphism ⟩
|
||||
μ.η _ ∘ F.₁ (η.η _) ∘ F.₁ f ≈⟨ cancelˡ monad.identityˡ ⟩
|
||||
F.₁ f ∎
|
||||
where
|
||||
module monad = Monad M
|
||||
open monad using (F; η; μ)
|
||||
F₁⇒extend : ∀ (M : Monad C) {X Y} (f : X ⇒ Y) → RMonad.extend (Monad⇒Kleisli C M) (RMonad.unit (Monad⇒Kleisli C M) ∘ f) ≈ Monad.F.₁ M f
|
||||
F₁⇒extend M f = begin
|
||||
μ.η _ ∘ F.₁ (η.η _ ∘ f) ≈⟨ refl⟩∘⟨ F.homomorphism ⟩
|
||||
μ.η _ ∘ F.₁ (η.η _) ∘ F.₁ f ≈⟨ cancelˡ m-identityˡ ⟩
|
||||
F.₁ f ∎
|
||||
where open Monad M using (F; η; μ) renaming (identityˡ to m-identityˡ)
|
||||
```
|
||||
|
|
@ -105,14 +105,8 @@ At the same time the morphism `X × N ⇒ X + X × N` is a coalgebra for the `(Y
|
|||
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
|
||||
ι = u (! {A = record { A = X × N ; α = _≅_.from nno-iso }})
|
||||
```
|
||||
|
||||
## Delay is a monad
|
||||
|
|
|
|||
|
|
@ -30,6 +30,15 @@ module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D
|
|||
open import Categories.Morphism.Properties C
|
||||
open Terminal using (!; !-unique; ⊤)
|
||||
|
||||
-- TODO should be in agda-categories
|
||||
Kleisli⇒Monad⇒Kleisli : ∀ (K : KleisliTriple C) {X Y} (f : X ⇒ RMonad.F₀ K Y) → RMonad.extend (Monad⇒Kleisli C (Kleisli⇒Monad C K)) f ≈ RMonad.extend K f
|
||||
Kleisli⇒Monad⇒Kleisli K {X} {Y} f = begin
|
||||
extend idC ∘ extend (unit ∘ f) ≈⟨ sym k-assoc ⟩
|
||||
extend (extend idC ∘ unit ∘ f) ≈⟨ extend-≈ (pullˡ k-identityʳ) ⟩
|
||||
extend (idC ∘ f) ≈⟨ extend-≈ (identityˡ) ⟩
|
||||
extend f ∎
|
||||
where open RMonad K using (unit; extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
|
||||
|
||||
open DelayM D
|
||||
open import Monad.Instance.Delay.Strong ambient D
|
||||
open Functor functor using () renaming (F₁ to D₁; identity to D-identity; homomorphism to D-homomorphism; F-resp-≈ to D-resp-≈)
|
||||
|
|
@ -183,7 +192,7 @@ module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D
|
|||
|
||||
fixpoint-eq : ∀ {f : D₀ X × D₀ Y ⇒ D₀ (X × Y)} → f ≈ out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ f ] ] ∘ w → f ≈ extend [ now , f ] ∘ g
|
||||
fixpoint-eq {f} fix = begin
|
||||
f ≈⟨ fix ⟩
|
||||
f ≈⟨ fix ⟩
|
||||
out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , ▷ ∘ f ] ] ∘ w ≈˘⟨ refl⟩∘⟨ []-cong₂ refl (refl⟩∘⟨ ([]-cong₂ refl (pullʳ inject₂))) ⟩∘⟨refl ⟩
|
||||
out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , (▷ ∘ [ now , f ]) ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ []-cong₂ refl (sym ∘[] ○ refl⟩∘⟨ []-cong₂ (elimˡ (extend-≈ inject₁ ○ k-identityˡ)) (pullˡ k-identityʳ)) ⟩∘⟨refl ⟩
|
||||
out⁻¹ ∘ [ idC +₁ σ , [ i₂ ∘ extend ([ now , f ] ∘ i₁) ∘ τ , i₂ ∘ extend (▷ ∘ [ now , f ]) ∘ now ∘ i₂ ] ] ∘ w ≈˘⟨ refl⟩∘⟨ []-cong₂ ([]-cong₂ (sym identityʳ) (refl⟩∘⟨ (elimˡ ((extend-≈ inject₁) ○ k-identityˡ)))) ([]-cong₂ (pullʳ (pullˡ ((sym k-assoc) ○ extend-≈ (pullˡ k-identityʳ)))) (pullʳ (pullˡ (▷∘extendʳ [ now , f ])))) ⟩∘⟨refl ⟩
|
||||
|
|
|
|||
|
|
@ -1,30 +0,0 @@
|
|||
<!--
|
||||
```agda
|
||||
open import Level
|
||||
open import Category.Instance.AmbientCategory
|
||||
open import Categories.Functor
|
||||
open import Categories.Monad.Relative using () renaming (Monad to RMonad)
|
||||
```
|
||||
-->
|
||||
|
||||
```agda
|
||||
module Monad.Instance.Delay.Lemmas {o ℓ e} (ambient : Ambient o ℓ e) where
|
||||
open Ambient ambient
|
||||
open import Monad.Instance.Delay ambient
|
||||
open import Monad.Instance.Delay.Strong ambient
|
||||
open import Monad.Instance.Delay.Commutative ambient
|
||||
open M C
|
||||
```
|
||||
|
||||
# Helper Lemmas concerning the Delay Monad
|
||||
|
||||
```agda
|
||||
module _ (D : DelayM) where
|
||||
open DelayM D
|
||||
module D = Functor functor
|
||||
open RMonad kleisli using (extend)
|
||||
|
||||
|
||||
Lemma47 : ⟨ D.₁ π₁ , D.₁ π₂ ⟩ SectionOf {! !}
|
||||
Lemma47 = {! !}
|
||||
```
|
||||
|
|
@ -10,8 +10,6 @@ open import Categories.Adjoint
|
|||
open import Categories.Adjoint.Properties
|
||||
open import Categories.Monad
|
||||
open import Categories.Monad.Strong
|
||||
open import Categories.Monad.Relative renaming (Monad to RMonad)
|
||||
open import Categories.Monad.Construction.Kleisli
|
||||
open import Category.Instance.AmbientCategory using (Ambient)
|
||||
open import Categories.NaturalTransformation
|
||||
open import Categories.Object.Terminal
|
||||
|
|
@ -37,12 +35,10 @@ In this file I explore the monad ***K*** and its properties:
|
|||
module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
|
||||
open Ambient ambient
|
||||
open import Category.Construction.UniformIterationAlgebras ambient
|
||||
open import Algebra.UniformIterationAlgebra ambient
|
||||
open import Algebra.UniformIterationAlgebra
|
||||
open import Algebra.Properties ambient using (FreeUniformIterationAlgebra; uniformForgetfulF; IsStableFreeUniformIterationAlgebra)
|
||||
|
||||
open Equiv
|
||||
open MR C
|
||||
open M C
|
||||
open HomReasoning
|
||||
|
||||
```
|
||||
|
|
@ -52,13 +48,13 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
|
|||
```agda
|
||||
record MonadK : Set (suc o ⊔ suc ℓ ⊔ suc e) where
|
||||
field
|
||||
freealgebras : ∀ X → FreeUniformIterationAlgebra X
|
||||
algebras : ∀ X → FreeUniformIterationAlgebra X
|
||||
|
||||
freeF : Functor C Uniform-Iteration-Algebras
|
||||
freeF = FO⇒Functor uniformForgetfulF freealgebras
|
||||
freeF = FO⇒Functor uniformForgetfulF algebras
|
||||
|
||||
adjoint : freeF ⊣ uniformForgetfulF
|
||||
adjoint = FO⇒LAdj uniformForgetfulF freealgebras
|
||||
adjoint = FO⇒LAdj uniformForgetfulF algebras
|
||||
|
||||
K : Monad C
|
||||
K = adjoint⇒monad adjoint
|
||||
|
|
@ -69,214 +65,61 @@ module Monad.Instance.K {o ℓ e} (ambient : Ambient o ℓ e) where
|
|||
```agda
|
||||
record MonadKStrong : Set (suc o ⊔ suc ℓ ⊔ suc e) where
|
||||
field
|
||||
freealgebras : ∀ X → FreeUniformIterationAlgebra X
|
||||
stable : ∀ X → IsStableFreeUniformIterationAlgebra (freealgebras X)
|
||||
algebras : ∀ X → FreeUniformIterationAlgebra X
|
||||
stable : ∀ X → IsStableFreeUniformIterationAlgebra (algebras X)
|
||||
|
||||
algebras : ∀ (X : Obj) → Uniform-Iteration-Algebra
|
||||
algebras X = FreeObject.FX (freealgebras X)
|
||||
|
||||
K : Monad C
|
||||
K = MonadK.K (record { freealgebras = freealgebras })
|
||||
K = MonadK.K (record { algebras = algebras })
|
||||
|
||||
open Monad K using (F; μ) renaming (identityʳ to m-identityʳ)
|
||||
module kleisli = RMonad (Monad⇒Kleisli C K)
|
||||
open kleisli using (extend)
|
||||
open Monad K using (F)
|
||||
open Functor F using () renaming (F₀ to K₀; F₁ to K₁)
|
||||
|
||||
KStrong : StrongMonad {C = C} monoidal
|
||||
KStrong = record
|
||||
{ M = K
|
||||
{ M = K
|
||||
; strength = record
|
||||
{ strengthen = ntHelper (record { η = τ ; commute = commute' })
|
||||
; identityˡ = identityˡ'
|
||||
; η-comm = λ {A} {B} → τ-η (A , B)
|
||||
; μ-η-comm = μ-η-comm'
|
||||
; strength-assoc = strength-assoc'
|
||||
{ strengthen = ntHelper (record { η = τ ; commute = commute' })
|
||||
; identityˡ = λ {X} → begin
|
||||
K₁ π₂ ∘ τ _ ≈⟨ refl ⟩
|
||||
Uniform-Iteration-Algebra-Morphism.h ((algebras (Terminal.⊤ terminal × X) FreeObject.*) (FreeObject.η (algebras X) ∘ π₂)) ∘ τ _ ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
π₂ ∎
|
||||
; η-comm = λ {A} {B} → begin τ _ ∘ (idC ⁂ η (A , B) B) ≈⟨ τ-η (A , B) ⟩ η (A , B) (A × B) ∎
|
||||
; μ-η-comm = λ {A} {B} → {! !}
|
||||
; strength-assoc = λ {A} {B} {D} → begin
|
||||
K₁ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∘ τ _ ≈⟨ {! !} ⟩
|
||||
τ _ ∘ (idC ⁂ τ _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ∎
|
||||
}
|
||||
}
|
||||
where
|
||||
open import Agda.Builtin.Sigma
|
||||
open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving; ♯-unique)
|
||||
open Uniform-Iteration-Algebra using (#-Uniformity; #-Fixpoint; #-resp-≈)
|
||||
η = λ Z → FreeObject.η (freealgebras Z)
|
||||
_♯ = λ {A X Y} f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} (algebras Y) f
|
||||
_# = λ {A} {X} f → Uniform-Iteration-Algebra._# (algebras A) {X = X} f
|
||||
open IsStableFreeUniformIterationAlgebra using (♯-law; ♯-preserving)
|
||||
|
||||
module _ (P : Category.Obj (CProduct C C)) where
|
||||
private
|
||||
X = fst P
|
||||
Y = snd P
|
||||
η = λ Z → FreeObject.η (algebras Z)
|
||||
[_,_,_]♯ = λ {A} X Y f → IsStableFreeUniformIterationAlgebra.[_,_]♯ {Y = X} (stable X) {X = A} Y f
|
||||
|
||||
|
||||
X = fst P
|
||||
Y = snd P
|
||||
τ : X × K₀ Y ⇒ K₀ (X × Y)
|
||||
τ = η (X × Y) ♯
|
||||
τ = [ Y , FreeObject.FX (algebras (X × Y)) , η (X × Y) ]♯
|
||||
|
||||
τ-η : τ ∘ (idC ⁂ η Y) ≈ η (X × Y)
|
||||
τ-η = sym (♯-law (stable Y) (η (X × Y)))
|
||||
|
||||
τ-comm : ∀ {X Y Z : Obj} (h : Z ⇒ K₀ Y + Z) → τ (X , Y) ∘ (idC ⁂ h #) ≈ ((τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
|
||||
τ-comm {X} {Y} {Z} h = ♯-preserving (stable Y) (η (X × Y)) h
|
||||
[_,_]# : ∀ (A : Uniform-Iteration-Algebra ambient) {X} → (X ⇒ ((Uniform-Iteration-Algebra.A A) + X)) → (X ⇒ Uniform-Iteration-Algebra.A A)
|
||||
[ A , f ]# = Uniform-Iteration-Algebra._# A f
|
||||
|
||||
K₁η : ∀ {X Y} (f : X ⇒ Y) → K₁ f ∘ η X ≈ η Y ∘ f
|
||||
K₁η {X} {Y} f = begin
|
||||
K₁ f ∘ η X ≈⟨ (sym (F₁⇒extend K f)) ⟩∘⟨refl ⟩
|
||||
extend (η Y ∘ f) ∘ η X ≈⟨ kleisli.identityʳ ⟩
|
||||
η Y ∘ f ∎
|
||||
τ-comm : ∀ {X Y Z : Obj} (h : Z ⇒ K₀ Y + Z) → τ (X , Y) ∘ (idC ⁂ [ FreeObject.FX (algebras Y) , h ]#) ≈ [ FreeObject.FX (algebras (X × Y)) , (τ (X , Y) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ]#
|
||||
τ-comm {X} {Y} {Z} h = ♯-preserving (stable Y) (η (X , Y) (X × Y)) h
|
||||
|
||||
μ-η-comm' : ∀ {A B} → μ.η _ ∘ K₁ (τ _) ∘ τ (A , K₀ B) ≈ τ _ ∘ (idC ⁂ μ.η _)
|
||||
μ-η-comm' {A} {B} = begin
|
||||
μ.η _ ∘ K₁ (τ _) ∘ τ _ ≈⟨ ♯-unique (stable (K₀ B)) (τ (A , B)) (μ.η _ ∘ K₁ (τ _) ∘ τ _) comm₁ comm₂ ⟩
|
||||
(τ _ ♯) ≈⟨ sym (♯-unique (stable (K₀ B)) (τ (A , B)) (τ _ ∘ (idC ⁂ μ.η _)) (sym (cancelʳ (⁂∘⁂ ○ ⁂-cong₂ identity² m-identityʳ ○ ⟨⟩-unique id-comm id-comm))) comm₃) ⟩
|
||||
τ _ ∘ (idC ⁂ μ.η _) ∎
|
||||
where
|
||||
comm₁ : τ (A , B) ≈ (μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ η _)
|
||||
comm₁ = sym (begin
|
||||
(μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ η _) ≈⟨ pullʳ (pullʳ (τ-η _)) ⟩
|
||||
μ.η _ ∘ K₁ (τ _) ∘ η _ ≈⟨ refl⟩∘⟨ (K₁η (τ (A , B))) ⟩
|
||||
μ.η _ ∘ η _ ∘ τ _ ≈⟨ cancelˡ m-identityʳ ⟩
|
||||
τ _ ∎)
|
||||
comm₂ : ∀ {Z : Obj} (h : Z ⇒ K₀ (K₀ B) + Z) → (μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ h #) ≈ ((μ.η _ ∘ K₁ (τ (A , B)) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
|
||||
comm₂ {Z} h = begin
|
||||
(μ.η _ ∘ K₁ (τ _) ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (pullʳ (τ-comm h)) ⟩
|
||||
μ.η _ ∘ K₁ (τ _) ∘ (((τ (A , K₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ≈⟨ refl⟩∘⟨ (Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η _ ∘ τ _))) ⟩
|
||||
μ.η _ ∘ ((K₁ (τ _) +₁ idC) ∘ (τ (A , K₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC) ⟩
|
||||
((μ.η _ +₁ idC) ∘ (K₁ (τ _) +₁ idC) ∘ (τ (A , K₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
|
||||
((μ.η _ ∘ K₁ (τ _) +₁ idC ∘ idC) ∘ (τ (A , K₀ B) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ +₁∘+₁) ⟩
|
||||
(((μ.η _ ∘ K₁ (τ _)) ∘ τ _ +₁ (idC ∘ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) ((+₁-cong₂ assoc (cancelʳ identity²)) ⟩∘⟨refl) ⟩
|
||||
((μ.η _ ∘ K₁ (τ (A , B)) ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
|
||||
comm₃ : ∀ {Z : Obj} (h : Z ⇒ K₀ (K₀ B) + Z) → (τ _ ∘ (idC ⁂ μ.η _)) ∘ (idC ⁂ h #) ≈ ((τ _ ∘ (idC ⁂ μ.η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
|
||||
comm₃ {Z} h = begin
|
||||
(τ _ ∘ (idC ⁂ μ.η _)) ∘ (idC ⁂ h #) ≈⟨ pullʳ ⁂∘⁂ ⟩
|
||||
τ _ ∘ (idC ∘ idC ⁂ μ.η _ ∘ h #) ≈⟨ refl⟩∘⟨ (⁂-cong₂ identity² (Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) idC))) ⟩
|
||||
τ _ ∘ (idC ⁂ ((μ.η _ +₁ idC) ∘ h) #) ≈⟨ τ-comm ((μ.η B +₁ idC) ∘ h) ⟩
|
||||
((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (μ.η B +₁ idC) ∘ h)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (refl⟩∘⟨ (⁂-cong₂ (sym identity²) refl ○ sym ⁂∘⁂))) ⟩
|
||||
((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (μ.η B +₁ idC)) ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (refl⟩∘⟨ (pullˡ (sym (distribute₁ idC (μ.η B) idC)))) ⟩
|
||||
((τ _ +₁ idC) ∘ ((idC ⁂ μ.η B +₁ idC ⁂ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) (pullˡ (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl (elimʳ (⟨⟩-unique id-comm id-comm))))) ⟩
|
||||
(((τ _ ∘ (idC ⁂ μ.η B) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras _) assoc ⟩
|
||||
((τ _ ∘ (idC ⁂ μ.η _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
|
||||
|
||||
module assoc {A} {B} {C} = _≅_ (×-assoc {A} {B} {C})
|
||||
|
||||
strength-assoc' : ∀ {X Y Z} → K₁ assoc.to ∘ τ (X × Y , Z) ≈ τ (X , Y × Z) ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to
|
||||
strength-assoc' {X} {Y} {Z} = begin
|
||||
K₁ assoc.to ∘ τ _ ≈⟨ ♯-unique (stable _) (η (X × Y × Z) ∘ assoc.to) (K₁ assoc.to ∘ τ _) (sym (pullʳ (τ-η _) ○ K₁η _)) comm₁ ⟩
|
||||
((η (X × Y × Z) ∘ assoc.to) ♯) ≈⟨ sym (♯-unique (stable _) (η (X × Y × Z) ∘ assoc.to) (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) comm₂ comm₃) ⟩
|
||||
τ _ ∘ (idC ⁂ τ _) ∘ assoc.to ∎
|
||||
where
|
||||
comm₁ : ∀ {A : Obj} (h : A ⇒ K₀ Z + A) → (K₁ assoc.to ∘ τ _) ∘ (idC ⁂ h #) ≈ ((K₁ assoc.to ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
|
||||
comm₁ {A} h = begin
|
||||
(K₁ assoc.to ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (τ-comm h) ⟩
|
||||
K₁ assoc.to ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) _) ⟩
|
||||
((K₁ assoc.to +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ≈⟨ #-resp-≈ (algebras _) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
|
||||
((K₁ assoc.to ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
|
||||
comm₂ : η (X × Y × Z) ∘ assoc.to ≈ (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (idC ⁂ η _)
|
||||
comm₂ = sym (begin
|
||||
(τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (idC ⁂ η _) ≈⟨ (refl⟩∘⟨ ⁂∘⟨⟩) ⟩∘⟨refl ⟩
|
||||
(τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ η _) ≈⟨ pullʳ ⟨⟩∘ ⟩
|
||||
τ _ ∘ ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ η _) , (τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ η _) ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (identityˡ ⟩∘⟨refl ○ pullʳ π₁∘⁂) (pullʳ ⟨⟩∘)) ⟩
|
||||
τ _ ∘ ⟨ π₁ ∘ idC ∘ π₁ , τ _ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ η _) , π₂ ∘ (idC ⁂ η _) ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂))) ⟩
|
||||
τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ idC ∘ π₁ , η _ ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (refl⟩∘⟨ ((⟨⟩-cong₂ (sym identityˡ) refl) ○ sym ⁂∘⟨⟩))) ⟩
|
||||
τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , τ _ ∘ (idC ⁂ η _) ∘ ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (pullˡ (τ-η (Y , Z)))) ⟩
|
||||
τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , η _ ∘ ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (sym ⁂∘⟨⟩) ⟩
|
||||
τ _ ∘ (idC ⁂ η _) ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ pullˡ (τ-η _) ⟩
|
||||
η _ ∘ ⟨ π₁ ∘ π₁ , ⟨ π₂ ∘ idC ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) refl) ⟩
|
||||
η (X × Y × Z) ∘ assoc.to ∎)
|
||||
comm₃ : ∀ {A : Obj} (h : A ⇒ K₀ Z + A) → (τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (idC ⁂ h #) ≈ ((τ _ ∘ (idC ⁂ τ _) ∘ assoc.to +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
|
||||
comm₃ {A} h = begin
|
||||
(τ _ ∘ (idC ⁂ τ _) ∘ assoc.to) ∘ (idC ⁂ h #) ≈⟨ (refl⟩∘⟨ ⁂∘⟨⟩) ⟩∘⟨refl ⟩
|
||||
(τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩) ∘ (idC ⁂ h #) ≈⟨ pullʳ ⟨⟩∘ ⟩
|
||||
τ _ ∘ ⟨ (idC ∘ π₁ ∘ π₁) ∘ (idC ⁂ h #) , (τ _ ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩) ∘ (idC ⁂ h #) ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (identityˡ ⟩∘⟨refl ○ pullʳ π₁∘⁂) (pullʳ ⟨⟩∘)) ⟩
|
||||
τ _ ∘ ⟨ π₁ ∘ idC ∘ π₁ , τ _ ∘ ⟨ (π₂ ∘ π₁) ∘ (idC ⁂ h #) , π₂ ∘ (idC ⁂ h #) ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (refl⟩∘⟨ identityˡ) (refl⟩∘⟨ (⟨⟩-cong₂ (pullʳ π₁∘⁂) π₂∘⁂)) ⟩
|
||||
τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ ⟨ π₂ ∘ idC ∘ π₁ , h # ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ refl (refl⟩∘⟨ (⟨⟩-cong₂ ((refl⟩∘⟨ identityˡ) ○ sym identityˡ) refl))) ⟩
|
||||
τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ ⟨ idC ∘ π₂ ∘ π₁ , h # ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ refl (refl⟩∘⟨ (sym ⁂∘⟨⟩)) ⟩
|
||||
τ _ ∘ ⟨ π₁ ∘ π₁ , τ _ ∘ (idC ⁂ h #) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (⟨⟩-cong₂ (sym identityˡ) (pullˡ (τ-comm h))) ⟩
|
||||
τ _ ∘ ⟨ idC ∘ π₁ ∘ π₁ , (((τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ ⟨ π₂ ∘ π₁ , π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ (sym ⁂∘⟨⟩) ⟩
|
||||
τ _ ∘ (idC ⁂ ((τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #) ∘ assoc.to ≈⟨ pullˡ (τ-comm _) ⟩
|
||||
((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) # ∘ assoc.to ≈⟨ sym (#-Uniformity (algebras _) (begin
|
||||
(idC +₁ assoc.to) ∘ (τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩
|
||||
(idC ∘ τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to +₁ assoc.to ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩
|
||||
(τ _ ∘ (idC ⁂ τ (Y , Z)) ∘ assoc.to +₁ idC ∘ assoc.to) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈˘⟨ (+₁∘+₁ ○ +₁-cong₂ assoc refl) ⟩∘⟨refl ⟩
|
||||
((τ _ ∘ (idC ⁂ τ (Y , Z)) +₁ idC) ∘ (assoc.to +₁ assoc.to)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullʳ (pullˡ (sym distributeˡ⁻¹-assoc)) ⟩
|
||||
(τ _ ∘ (idC ⁂ τ (Y , Z)) +₁ idC) ∘ (distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assoc.to) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ assoc²' ⟩
|
||||
(τ _ ∘ (idC ⁂ τ _) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assoc.to ∘ (idC ⁂ h) ≈˘⟨ (+₁-cong₂ refl (elimʳ (⟨⟩-unique id-comm id-comm))) ⟩∘⟨refl ⟩
|
||||
(τ _ ∘ (idC ⁂ τ _) +₁ idC ∘ (idC ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ distributeˡ⁻¹) ∘ assoc.to ∘ (idC ⁂ h) ≈˘⟨ assoc ○ assoc ⟩
|
||||
(((τ _ ∘ (idC ⁂ τ _) +₁ idC ∘ (idC ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ _≅_.to ×-assoc ∘ (idC ⁂ h) ≈˘⟨ pullˡ (pullˡ (pullˡ +₁∘+₁)) ⟩
|
||||
(τ _ +₁ idC) ∘ ((((idC ⁂ τ _) +₁ (idC ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assoc.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ ((distribute₁ idC (τ (Y , Z)) idC) ⟩∘⟨refl) ⟩∘⟨refl ⟩
|
||||
(τ _ +₁ idC) ∘ ((distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC))) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assoc.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ (assoc ○ assoc ○ refl⟩∘⟨ sym-assoc) ⟩
|
||||
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((idC ⁂ (τ (Y , Z) +₁ idC)) ∘ (idC ⁂ distributeˡ⁻¹)) ∘ assoc.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂∘⁂ ○ ⁂-cong₂ identity² refl) ⟩∘⟨refl ⟩
|
||||
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ assoc.to ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂-cong₂ (sym (⟨⟩-unique id-comm id-comm)) refl ⟩
|
||||
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ assoc.to ∘ ((idC ⁂ idC) ⁂ h) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ assocˡ∘⁂ ⟩
|
||||
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ h)) ∘ assoc.to ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
|
||||
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ ((idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ (idC ⁂ h))) ∘ assoc.to ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⁂∘⁂ ⟩∘⟨refl ⟩
|
||||
(τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ∘ idC ⁂ ((τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹) ∘ (idC ⁂ h)) ∘ assoc.to ≈⟨ refl⟩∘⟨ (refl⟩∘⟨ ((⁂-cong₂ identity² assoc) ⟩∘⟨refl) ○ sym-assoc) ○ sym-assoc ⟩
|
||||
((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (τ (Y , Z) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))) ∘ assoc.to ∎)) ⟩
|
||||
((τ _ ∘ (idC ⁂ τ _) ∘ assoc.to +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
|
||||
|
||||
commute' : ∀ {P₁ : Category.Obj (CProduct C C)} {P₂ : Category.Obj (CProduct C C)} (fg : _[_,_] (CProduct C C) P₁ P₂)
|
||||
→ τ P₂ ∘ ((fst fg) ⁂ K₁ (snd fg)) ≈ K₁ ((fst fg) ⁂ (snd fg)) ∘ τ P₁
|
||||
commute' {(U , V)} {(W , X)} (f , g) = begin
|
||||
τ _ ∘ (f ⁂ K₁ g) ≈⟨ ♯-unique (stable V) (η (W × X) ∘ (f ⁂ g)) (τ _ ∘ (f ⁂ K₁ g)) comm₁ comm₂ ⟩
|
||||
(η _ ∘ (f ⁂ g)) ♯ ≈⟨ sym (♯-unique (stable V) (η (W × X) ∘ (f ⁂ g)) (K₁ (f ⁂ g) ∘ τ _) comm₃ comm₄) ⟩
|
||||
K₁ (f ⁂ g) ∘ τ _ ∎
|
||||
where
|
||||
comm₁ : η (W × X) ∘ (f ⁂ g) ≈ (τ (W , X) ∘ (f ⁂ K₁ g)) ∘ (idC ⁂ η V)
|
||||
comm₁ = sym (begin
|
||||
(τ (W , X) ∘ (f ⁂ K₁ g)) ∘ (idC ⁂ η V) ≈⟨ pullʳ ⁂∘⁂ ⟩
|
||||
τ (W , X) ∘ (f ∘ idC ⁂ K₁ g ∘ η V) ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm (K₁η g)) ⟩
|
||||
τ (W , X) ∘ (idC ∘ f ⁂ η X ∘ g) ≈⟨ refl⟩∘⟨ (sym ⁂∘⁂) ⟩
|
||||
τ (W , X) ∘ (idC ⁂ η X) ∘ (f ⁂ g) ≈⟨ pullˡ (τ-η (W , X)) ⟩
|
||||
η (W × X) ∘ (f ⁂ g) ∎)
|
||||
comm₃ : η (W × X) ∘ (f ⁂ g) ≈ (K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ η V)
|
||||
comm₃ = sym (begin
|
||||
(K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ η V) ≈⟨ pullʳ (τ-η (U , V)) ⟩
|
||||
K₁ (f ⁂ g) ∘ η (U × V) ≈⟨ K₁η (f ⁂ g) ⟩
|
||||
η (W × X) ∘ (f ⁂ g) ∎)
|
||||
comm₂ : ∀ {Z : Obj} (h : Z ⇒ K₀ V + Z) → (τ (W , X) ∘ (f ⁂ K₁ g)) ∘ (idC ⁂ h #) ≈ ((τ (W , X) ∘ (f ⁂ K₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
|
||||
comm₂ {Z} h = begin
|
||||
(τ (W , X) ∘ (f ⁂ K₁ g)) ∘ (idC ⁂ h #) ≈⟨ pullʳ ⁂∘⁂ ⟩
|
||||
τ (W , X) ∘ (f ∘ idC ⁂ K₁ g ∘ (h #)) ≈⟨ refl⟩∘⟨ (⁂-cong₂ id-comm ((Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η X ∘ g))) ○ sym identityʳ)) ⟩
|
||||
τ (W , X) ∘ (idC ∘ f ⁂ ((K₁ g +₁ idC) ∘ h) # ∘ idC) ≈⟨ refl⟩∘⟨ (sym ⁂∘⁂) ⟩
|
||||
τ (W , X) ∘ (idC ⁂ ((K₁ g +₁ idC) ∘ h) #) ∘ (f ⁂ idC) ≈⟨ pullˡ (♯-preserving (stable _) (η _) ((K₁ g +₁ idC) ∘ h)) ⟩
|
||||
((τ (W , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (K₁ g +₁ idC) ∘ h)) # ∘ (f ⁂ idC) ≈⟨ sym (#-Uniformity (algebras _) (begin
|
||||
(idC +₁ f ⁂ idC) ∘ (τ (W , X) ∘ (f ⁂ K₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩
|
||||
(idC ∘ τ (W , X) ∘ (f ⁂ K₁ g) +₁ (f ⁂ idC) ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (+₁-cong₂ identityˡ id-comm) ⟩∘⟨refl ⟩
|
||||
(τ (W , X) ∘ (f ⁂ K₁ g) +₁ idC ∘ (f ⁂ idC)) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (sym +₁∘+₁) ⟩∘⟨refl ⟩
|
||||
((τ (W , X) +₁ idC) ∘ ((f ⁂ K₁ g) +₁ (f ⁂ idC))) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullʳ (pullˡ (distribute₁ f (K₁ g) idC)) ⟩
|
||||
(τ (W , X) +₁ idC) ∘ (distributeˡ⁻¹ ∘ (f ⁂ (K₁ g +₁ idC))) ∘ (idC ⁂ h) ≈⟨ refl⟩∘⟨ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityʳ refl)) ⟩
|
||||
(τ (W , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (f ⁂ (K₁ g +₁ idC) ∘ h) ≈˘⟨ pullʳ (pullʳ (⁂∘⁂ ○ ⁂-cong₂ identityˡ identityʳ)) ⟩
|
||||
((τ (W , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ (K₁ g +₁ idC) ∘ h)) ∘ (f ⁂ idC) ∎)) ⟩
|
||||
((τ (W , X) ∘ (f ⁂ K₁ g) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
|
||||
comm₄ : ∀ {Z : Obj} (h : Z ⇒ K₀ V + Z) → (K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ h #) ≈ ((K₁ (f ⁂ g) ∘ τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
|
||||
comm₄ {Z} h = begin
|
||||
(K₁ (f ⁂ g) ∘ τ (U , V)) ∘ (idC ⁂ (h #)) ≈⟨ pullʳ (τ-comm h) ⟩
|
||||
K₁ (f ⁂ g) ∘ ((τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves (((freealgebras _) FreeObject.*) (η (W × X) ∘ (f ⁂ g))) ⟩
|
||||
((K₁ (f ⁂ g) +₁ idC) ∘ (τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras (W × X)) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
|
||||
((K₁ (f ⁂ g) ∘ τ (U , V) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
|
||||
|
||||
identityˡ' : ∀ {X : Obj} → K₁ π₂ ∘ τ _ ≈ π₂
|
||||
identityˡ' {X} = begin
|
||||
K₁ π₂ ∘ τ _ ≈⟨ ♯-unique (stable X) (η X ∘ π₂) (K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) comm₁ comm₂ ⟩
|
||||
(η X ∘ π₂) ♯ ≈⟨ sym (♯-unique (stable X) (η X ∘ π₂) π₂ (sym π₂∘⁂) comm₃) ⟩
|
||||
π₂ ∎
|
||||
where
|
||||
comm₁ : η X ∘ π₂ ≈ (K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) ∘ (idC ⁂ η X)
|
||||
comm₁ = sym (begin
|
||||
(K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) ∘ (idC ⁂ η X) ≈⟨ pullʳ (τ-η (Terminal.⊤ terminal , X)) ⟩
|
||||
K₁ π₂ ∘ η (Terminal.⊤ terminal × X) ≈⟨ (sym (F₁⇒extend K π₂)) ⟩∘⟨refl ⟩
|
||||
extend (η _ ∘ π₂) ∘ η _ ≈⟨ kleisli.identityʳ ⟩
|
||||
η X ∘ π₂ ∎)
|
||||
comm₂ : ∀ {Z : Obj} (h : Z ⇒ K₀ X + Z) → (K₁ π₂ ∘ τ (Terminal.⊤ terminal , X)) ∘ (idC ⁂ h # ) ≈ ((K₁ π₂ ∘ τ (Terminal.⊤ terminal , X) +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))#
|
||||
comm₂ {Z} h = begin
|
||||
(K₁ π₂ ∘ τ _) ∘ (idC ⁂ h #) ≈⟨ pullʳ (♯-preserving (stable X) (η _) h) ⟩
|
||||
K₁ π₂ ∘ ((τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ Uniform-Iteration-Algebra-Morphism.preserves ((freealgebras (Terminal.⊤ terminal × X) FreeObject.*) (η X ∘ π₂)) ⟩
|
||||
((K₁ π₂ +₁ idC) ∘ (τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ≈⟨ #-resp-≈ (algebras X) (pullˡ (+₁∘+₁ ○ +₁-cong₂ refl identity²)) ⟩
|
||||
((K₁ π₂ ∘ τ _ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h))# ∎
|
||||
comm₃ : ∀ {Z : Obj} (h : Z ⇒ K₀ X + Z) → π₂ ∘ (idC ⁂ h #) ≈ ((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) #
|
||||
comm₃ {Z} h = begin
|
||||
π₂ ∘ (idC ⁂ h #) ≈⟨ π₂∘⁂ ⟩
|
||||
h # ∘ π₂ ≈⟨ sym (#-Uniformity (algebras X) (begin
|
||||
(idC +₁ π₂) ∘ (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ +₁∘+₁ ⟩
|
||||
(idC ∘ π₂ +₁ π₂ ∘ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ (+₁-cong₂ identityˡ identityʳ) ⟩∘⟨refl ⟩
|
||||
(π₂ +₁ π₂) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h) ≈⟨ pullˡ dstr-law₅ ⟩
|
||||
π₂ ∘ (idC ⁂ h) ≈⟨ project₂ ⟩
|
||||
h ∘ π₂ ∎)) ⟩
|
||||
((π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ h)) # ∎
|
||||
τ _ ∘ (f ⁂ Uniform-Iteration-Algebra-Morphism.h ((algebras V FreeObject.*) (FreeObject.η (algebras X) ∘ g))) ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
Uniform-Iteration-Algebra-Morphism.h ((algebras (U × V) FreeObject.*) (FreeObject.η (algebras (W × X)) ∘ (f ⁂ g))) ∘ τ _ ∎
|
||||
```
|
||||
|
|
|
|||
Loading…
Reference in a new issue