mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
Progress on strength for delay monad
This commit is contained in:
parent
7c5dccc0ab
commit
59492a9502
SSH key fingerprint:
SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
2 changed files with 94 additions and 17 deletions
|
|
@ -50,7 +50,9 @@ module Category.Instance.AmbientCategory where
|
|||
-- open Terminal terminal public
|
||||
-- Don't open the terminal object, because we are interested in many different terminal objects stemming from multiple categories
|
||||
open BinaryProducts products renaming (η to ⁂-η; g-η to ⁂-g-η; unique to ⟨⟩-unique; unique′ to ⟨⟩-unique′) public
|
||||
open ParametrizedNNO ℕ public
|
||||
open ParametrizedNNO ℕ public renaming (η to pnno-η)
|
||||
|
||||
open CartesianMonoidal cartesian using (⊤×A≅A; A×⊤≅A) public
|
||||
|
||||
|
||||
distributive : Distributive C
|
||||
|
|
|
|||
|
|
@ -1,5 +1,6 @@
|
|||
<!--
|
||||
```agda
|
||||
{-# OPTIONS --allow-unsolved-metas #-}
|
||||
open import Level
|
||||
open import Categories.Category
|
||||
open import Categories.Monad
|
||||
|
|
@ -294,30 +295,41 @@ Next we will show that the delay monad is strong, by giving a natural transforma
|
|||
open import Categories.Category.Monoidal.Core
|
||||
open Monoidal monoidal
|
||||
open import Categories.Monad.Relative using () renaming (Monad to RMonad)
|
||||
open RMonad kleisli using (extend)
|
||||
open RMonad kleisli using (extend) renaming (assoc to k-assoc)
|
||||
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ˡ = λ {X} → begin
|
||||
extend (now ∘ π₂) ∘ τ _ ≈⟨ introˡ (_≅_.isoˡ out-≅) ⟩
|
||||
(out⁻¹ ∘ out) ∘ extend (now ∘ π₂) ∘ τ _ ≈⟨ pullʳ (pullˡ (extendlaw (now ∘ π₂))) ⟩
|
||||
out⁻¹ ∘ ([ out ∘ now ∘ π₂ , i₂ ∘ extend (now ∘ π₂)] ∘ out) ∘ τ _ ≈⟨ refl⟩∘⟨ (pullʳ (τ-law (Terminal.⊤ terminal , X))) ⟩
|
||||
out⁻¹ ∘ [ out ∘ now ∘ π₂ , i₂ ∘ extend (now ∘ π₂)] ∘ (idC +₁ τ _) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ {! refl⟩∘⟨_ !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
-- TODO extend and τ are both final coalgebras, maybe use this?
|
||||
π₂ ∎
|
||||
; η-comm = {! !}
|
||||
; μ-η-comm = {! !}
|
||||
; identityˡ = identityˡ'
|
||||
; η-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 = begin
|
||||
extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈⟨ pullˡ (sym k-assoc) ⟩
|
||||
extend (extend idC ∘ now ∘ τ _) ∘ τ _ ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
τ _ ∘ (idC ⁂ extend idC) ∎
|
||||
; strength-assoc = {! !}
|
||||
}
|
||||
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ˡ))
|
||||
|
||||
module _ (P : Category.Obj (CProduct C C)) where
|
||||
X = fst P
|
||||
Y = snd P
|
||||
|
|
@ -329,9 +341,73 @@ Next we will show that the delay monad is strong, by giving a natural transforma
|
|||
τ-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ˡ⁻¹ ∎
|
||||
|
||||
τ-helper₂ : out ∘ extend (now ∘ π₂) ∘ τ ≈ out ∘ π₂
|
||||
τ-helper₂ = begin
|
||||
out ∘ extend (now ∘ π₂) ∘ τ ≈⟨ pullˡ (extendlaw (now ∘ π₂)) ⟩
|
||||
([ out ∘ now ∘ π₂ , i₂ ∘ extend (now ∘ π₂)] ∘ out) ∘ τ ≈⟨ (([]-cong₂ (pullˡ unitlaw) refl) ⟩∘⟨refl) ⟩∘⟨refl ⟩
|
||||
((π₂ +₁ extend (now ∘ π₂)) ∘ out) ∘ τ ≈⟨ pullʳ τ-law ⟩
|
||||
(π₂ +₁ extend (now ∘ π₂)) ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ +₁∘+₁ ⟩
|
||||
(π₂ ∘ idC +₁ extend (now ∘ π₂) ∘ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ (+₁-cong₂ identityʳ refl) ⟩∘⟨refl ⟩
|
||||
(π₂ +₁ extend (now ∘ π₂) ∘ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
{! !} ≈⟨ {! !} ⟩
|
||||
out ∘ π₂ ∎
|
||||
|
||||
τ-unique : (t : X × D₀ Y ⇒ D₀ (X × Y)) → (out ∘ t ≈ (idC +₁ t) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) → t ≈ τ
|
||||
τ-unique t t-commutes = sym (!-unique (record { f = t ; commutes = t-commutes }))
|
||||
|
||||
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ˡ⁻¹ ∎)
|
||||
{- ⁂ ⊤
|
||||
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
|
||||
|
|
@ -371,8 +447,7 @@ Next we will show that the delay monad is strong, by giving a natural transforma
|
|||
(distributeˡ⁻¹ ∘ [ ((f ⁂ (g +₁ h)) ∘ (idC ⁂ i₁)) , ((f ⁂ (g +₁ h)) ∘ (idC ⁂ i₂)) ]) ∘ distributeˡ⁻¹ ≈⟨ sym (pullˡ (pullʳ ∘[])) ⟩
|
||||
(distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h))) ∘ distributeˡ ∘ distributeˡ⁻¹ ≈⟨ sym (introʳ (IsIso.isoʳ isIsoˡ)) ⟩
|
||||
distributeˡ⁻¹ ∘ (f ⁂ (g +₁ h)) ∎
|
||||
-- ⁂ ○ ˡ
|
||||
-- ⁂ ○ ˡ ʳ
|
||||
strongMonad : StrongMonad monoidal
|
||||
strongMonad = record { M = monad ; strength = strength }
|
||||
```
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue