leonv/bsc-leon-vatthauer
1
0
Fork 0
mirror of https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git synced 2024-05-31 07:28:34 +02:00
Code Issues Projects Releases Packages Wiki Activity

🚧 Work on commutativity

Browse source
This commit is contained in:
Leon Vatthauer 2023-10-15 17:55:42 +02:00
parent 65d971eb68
commit 9ff33adfda
Signed by: leonv
SSH key fingerprint: SHA256:G4+ddwoZmhLPRB1agvXzZMXIzkVJ36dUYZXf5NxT+u8
5 changed files with 161 additions and 94 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Category/Instance/AmbientCategory.lagda.md
View file

@ -1,5 +1,6 @@
<!-- <!--
```agda ```agda
{-# OPTIONS --allow-unsolved-metas #-}
open import Level open import Level
open import Categories.Category.Core open import Categories.Category.Core
@ -17,6 +18,7 @@ open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Object.NaturalNumbers.Parametrized using (ParametrizedNNO) open import Categories.Object.NaturalNumbers.Parametrized using (ParametrizedNNO)
open import Categories.Object.Exponential using (Exponential) open import Categories.Object.Exponential using (Exponential)
open import Categories.Object.Terminal open import Categories.Object.Terminal
open import Categories.Morphism.Properties
import Categories.Morphism as M' import Categories.Morphism as M'
import Categories.Morphism.Reasoning as MR' import Categories.Morphism.Reasoning as MR'
``` ```
@ -70,6 +72,20 @@ module Category.Instance.AmbientCategory where
distributeʳ⁻¹ : ∀ {A B C : Obj} → (B + C) × A ⇒ B × A + C × A distributeʳ⁻¹ : ∀ {A B C : Obj} → (B + C) × A ⇒ B × A + C × A
distributeʳ⁻¹ = IsIso.inv isIsoʳ distributeʳ⁻¹ = IsIso.inv isIsoʳ
-- TODO add to agda-categories
distributeˡ⁻¹∘swap : ∀ {A B C : Obj} → distributeˡ⁻¹ ∘ swap ≈ (swap +₁ swap) ∘ distributeʳ⁻¹ {A} {B} {C}
distributeˡ⁻¹∘swap = Iso⇒Mono C (IsIso.iso isIsoˡ) (distributeˡ⁻¹ ∘ swap) ((swap +₁ swap) ∘ distributeʳ⁻¹) (begin
(distributeˡ ∘ distributeˡ⁻¹ ∘ swap) ≈⟨ cancelˡ (IsIso.isoʳ isIsoˡ) ⟩
swap ≈⟨ sym (cancelʳ (IsIso.isoʳ isIsoʳ)) ⟩
((swap ∘ distributeʳ) ∘ distributeʳ⁻¹) ≈⟨ ∘[] ⟩∘⟨refl ⟩
[ swap ∘ (i₁ ⁂ idC) , swap ∘ (i₂ ⁂ idC) ] ∘ distributeʳ⁻¹ ≈⟨ sym ([]-cong₂ (sym swap∘⁂) (sym swap∘⁂) ⟩∘⟨refl) ⟩
[ (idC ⁂ i₁) ∘ swap , (idC ⁂ i₂) ∘ swap ] ∘ distributeʳ⁻¹ ≈⟨ sym (pullˡ []∘+₁) ⟩
distributeˡ ∘ (swap +₁ swap) ∘ distributeʳ⁻¹ ∎)
where
open HomReasoning
open MR' C
open Equiv
module M = M' module M = M'
module MR = MR' module MR = MR'

8
src/Monad/Instance/Delay.lagda.md
View file

@ -10,11 +10,9 @@ open import Categories.Functor.Coalgebra
open import Categories.Functor renaming (id to idF) open import Categories.Functor renaming (id to idF)
open import Categories.Functor.Algebra open import Categories.Functor.Algebra
open import Categories.Monad.Construction.Kleisli open import Categories.Monad.Construction.Kleisli
open import Categories.Monad.Strong
open import Categories.Category.Construction.F-Coalgebras open import Categories.Category.Construction.F-Coalgebras
open import Categories.NaturalTransformation open import Categories.NaturalTransformation
open import Category.Instance.AmbientCategory using (Ambient) open import Category.Instance.AmbientCategory using (Ambient)
open import Monad.Commutative
``` ```
--> -->
```agda ```agda
@ -234,6 +232,12 @@ and second that `extend f` is the unique morphism satisfying the commutative dia
▷∘extendʳ : extend' f ∘ ▷ ≈ extend' (▷ ∘ f) ▷∘extendʳ : extend' f ∘ ▷ ≈ extend' (▷ ∘ f)
▷∘extendʳ = (sym ▷∘extend-comm) ○ ▷∘extendˡ ▷∘extendʳ = (sym ▷∘extend-comm) ○ ▷∘extendˡ
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 ∎
kleisli : KleisliTriple C kleisli : KleisliTriple C
kleisli = record kleisli = record
{ F₀ = D₀ { F₀ = D₀

89
src/Monad/Instance/Delay/Commutative.lagda.md
View file

@ -1,32 +1,115 @@
<!-- <!--
```agda ```agda
{-# OPTIONS --allow-unsolved-metas #-}
open import Level open import Level
open import Data.Product using (_,_; proj₁; proj₂)
open import Categories.Category.Core open import Categories.Category.Core
open import Categories.Functor open import Categories.Functor
open import Categories.Functor.Coalgebra
open import Category.Instance.AmbientCategory open import Category.Instance.AmbientCategory
open import Monad.Commutative open import Monad.Commutative
open import Monad.Instance.Delay open import Monad.Instance.Delay
open import Categories.Monad open import Categories.Monad
open import Categories.Monad.Strong open import Categories.Monad.Strong
open import Categories.Monad.Relative renaming (Monad to RMonad) open import Categories.Monad.Relative renaming (Monad to RMonad)
open import Categories.Monad.Construction.Kleisli
open import Categories.Object.Terminal
``` ```
--> -->
```agda ```agda
module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D : DelayM ambient) where module Monad.Instance.Delay.Commutative {o ℓ e} (ambient : Ambient o ℓ e) (D : DelayM ambient) where
open Ambient ambient open Ambient ambient
open HomReasoning
open Equiv
open MR C
open M C
open F-Coalgebra-Morphism using () renaming (f to u; commutes to u-commutes)
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 DelayM D
open import Monad.Instance.Delay.Strong ambient D open import Monad.Instance.Delay.Strong ambient D
open Functor open Functor functor using () renaming (F₁ to D₁)
open Monoidal monoidal
open RMonad kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ) open RMonad kleisli using (extend; extend-≈) renaming (assoc to k-assoc; identityʳ to k-identityʳ)
open Monad monad using (η; μ) open Monad monad using (η; μ)
open StrongMonad strongMonad using ()
``` ```
# The Delay Monad is commutative # The Delay Monad is commutative
```agda ```agda
commutativeMonad : CommutativeMonad symmetric strongMonad commutativeMonad : CommutativeMonad symmetric strongMonad
commutativeMonad = record { commutes = {! !} } commutativeMonad = record { commutes = λ {X} {Y} → pullˡ (Kleisli⇒Monad⇒Kleisli kleisli _) ○ commutes' ○ pushˡ (sym (Kleisli⇒Monad⇒Kleisli kleisli _)) }
where
open τ-mod hiding (τ)
τ : ∀ {X Y} → X × D₀ Y ⇒ D₀ (X × Y)
τ {X} {Y} = τ-mod.τ (X , Y)
σ : ∀ {X Y} → D₀ X × Y ⇒ D₀ (X × Y)
σ {X} {Y} = D₁ swap ∘ τ ∘ swap
σ-coalg : ∀ (X Y : Obj) → F-Coalgebra-Morphism {F = (X × Y) +- } (record { A = D₀ X × Y ; α = distributeʳ⁻¹ {Y} {X} {D₀ X} ∘ (out {X} ⁂ idC) }) (record { A = D₀ (X × Y) ; α = out {X × Y} })
σ-coalg X Y = record { f = σ ; commutes = begin
out ∘ σ ≈⟨ pullˡ (out-law swap) ⟩
((swap +₁ D₁ swap) ∘ out) ∘ τ ∘ swap ≈⟨ pullˡ (pullʳ (τ-law (Y , X))) ⟩
((swap +₁ D₁ swap) ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out)) ∘ swap ≈⟨ pullʳ (pullʳ (pullʳ (sym swap∘⁂))) ⟩
(swap +₁ D₁ swap) ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ swap ∘ (out ⁂ idC) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pullˡ distributeˡ⁻¹∘swap ⟩
(swap +₁ D₁ swap) ∘ (idC +₁ τ) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (out ⁂ idC) ≈⟨ pullˡ +₁∘+₁ ⟩
(swap ∘ idC +₁ D₁ swap ∘ τ) ∘ ((swap +₁ swap) ∘ distributeʳ⁻¹) ∘ (out ⁂ idC) ≈⟨ pullˡ (pullˡ +₁∘+₁) ⟩
(((swap ∘ idC) ∘ swap +₁ (D₁ swap ∘ τ) ∘ swap) ∘ distributeʳ⁻¹) ∘ (out ⁂ idC) ≈⟨ ((+₁-cong₂ (identityʳ ⟩∘⟨refl ○ swap∘swap) assoc) ⟩∘⟨refl) ⟩∘⟨refl ⟩
((idC +₁ D₁ swap ∘ τ ∘ swap) ∘ distributeʳ⁻¹) ∘ (out ⁂ idC) ≈⟨ assoc ⟩
(idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) ∎ }
commutes' : ∀ {X Y} → extend σ ∘ τ {D₀ X} {Y} ≈ extend τ ∘ σ
commutes' {X} {Y} = begin
extend σ ∘ τ ≈⟨ sym (!-unique (coalgebras (X × Y)) (record { f = extend σ ∘ τ ; commutes = begin
out ∘ extend σ ∘ τ ≈⟨ pullˡ (extendlaw σ) ⟩
([ out ∘ σ , i₂ ∘ extend σ ] ∘ out) ∘ τ ≈⟨ pullʳ (τ-law (D₀ X , Y)) ⟩
[ out ∘ σ , i₂ ∘ extend σ ] ∘ (idC +₁ τ) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ pullˡ []∘+₁ ⟩
[ (out ∘ σ) ∘ idC , (i₂ ∘ extend σ) ∘ τ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ ([]-cong₂ (identityʳ ○ u-commutes (σ-coalg X Y)) assoc) ⟩∘⟨refl ⟩
[ (idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) , i₂ ∘ extend σ ∘ τ ] ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ((⁂-cong₂ (sym (_≅_.isoˡ out-≅)) refl) ○ sym (⁂-cong₂ refl identityˡ) ○ sym ⁂∘⁂) ⟩
[ (idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) , i₂ ∘ extend σ ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out⁻¹ ⁂ idC) ∘ (out ⁂ out) ≈⟨ refl⟩∘⟨ refl⟩∘⟨ (⁂-cong₂ refl (sym ([]-unique id-comm-sym id-comm-sym))) ⟩∘⟨refl ⟩
[ (idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) , i₂ ∘ extend σ ∘ τ ] ∘ distributeˡ⁻¹ ∘ (out⁻¹ ⁂ (idC +₁ idC)) ∘ (out ⁂ out) ≈⟨ refl⟩∘⟨ pullˡ (sym (distribute₁ out⁻¹ idC idC)) ⟩
[ (idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC) , i₂ ∘ extend σ ∘ τ ] ∘ (((out⁻¹ ⁂ idC) +₁ (out⁻¹ ⁂ idC)) ∘ distributeˡ⁻¹) ∘ (out ⁂ out) ≈⟨ pullˡ (pullˡ []∘+₁) ⟩
([ ((idC +₁ σ) ∘ distributeʳ⁻¹ ∘ (out ⁂ idC)) ∘ (out⁻¹ ⁂ idC) , (i₂ ∘ extend σ ∘ τ) ∘ (out⁻¹ ⁂ idC) ] ∘ distributeˡ⁻¹) ∘ (out ⁂ out) ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
[ idC +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out) ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
{! !} ≈⟨ {! !} ⟩
(idC +₁ extend σ ∘ τ) ∘ {! !} ∎ })) ⟩
u (! (coalgebras (X × Y))) ≈⟨ {! !} ⟩
extend τ ∘ σ ∎
{-
out⁻¹ ∘ out ∘ extend σ ∘ τ
≈ out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , later ∘ extend σ ∘ τ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out)
≈ extend [ now , extend σ ∘ τ ] ∘ out⁻¹ ∘ [ i₁ +₁ (D₁ i₁) ∘ σ , i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out)
≈ extend [ now , extend σ ∘ τ ] ∘ out⁻¹ ∘ [ i₁ +₁ (D₁ i₁) ∘ σ , i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
out⁻¹ ∘ out ∘ extend τ ∘ σ
≈ out⁻¹ ∘ [ idC +₁ σ , i₂ ∘ [ τ , later ∘ extend τ ∘ σ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out)
≈ extend [ now , extend τ ∘ σ ] ∘ out⁻¹ ∘ [ i₁ +₁ (D₁ i₁) ∘ σ , i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ (distributeʳ⁻¹ +₁ distributeʳ⁻¹) ∘ distributeˡ⁻¹ ∘ (out ⁂ out)
≈ extend [ now , extend τ ∘ σ ] ∘ out⁻¹ ∘ [ i₁ +₁ (D₁ i₁) ∘ σ , i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
out ∘ extend [ now , extend σ ∘ τ ] ∘ out⁻¹ ∘ [ i₁ +₁ (D₁ i₁) ∘ σ , i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
[ out ∘ [ now , extend σ ∘ τ ] , i₂ ∘ extend [ now , extend σ ∘ τ ] ] ∘ out ∘ out⁻¹ ∘ [ i₁ +₁ (D₁ i₁) ∘ σ , i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
[ [ i₁ , out ∘ extend σ ∘ τ ] , i₂ ∘ extend [ now , extend σ ∘ τ ] ] ∘ [ i₁ +₁ (D₁ i₁) ∘ σ , i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
[ [ [ i₁ , out ∘ extend σ ∘ τ ] , i₂ ∘ extend [ now , extend σ ∘ τ ] ] ∘ (i₁ +₁ (D₁ i₁) ∘ σ) , [ [ i₁ , out ∘ extend σ ∘ τ ] , i₂ ∘ extend [ now , extend σ ∘ τ ] ] ∘ i₂ ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
[ [ [ i₁ , out ∘ extend σ ∘ τ ] ∘ i₁ , i₂ ∘ extend [ now , extend σ ∘ τ ] ∘ (D₁ i₁) ∘ σ ] , i₂ ∘ extend [ now , extend σ ∘ τ ] ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
[ [ i₁ , i₂ ∘ σ ] , i₂ ∘ extend [ now , extend σ ∘ τ ] ∘ [D₁ i₁ ∘ τ , now ∘ i₂ ] ] ∘ w
[ [ i₁ , i₂ ∘ σ ] , i₂ ∘ [extend [ now , extend σ ∘ τ ] ∘ D₁ i₁ ∘ τ , extend [ now , extend σ ∘ τ ] ∘ now ∘ i₂ ] ] ∘ w
[ [ i₁ , i₂ ∘ σ ] , i₂ ∘ [ τ , extend σ ∘ τ ] ] ∘ w
-}
``` ```

30
src/Monad/Instance/Delay/Quotienting.lagda.md
View file

@ -78,36 +78,6 @@ We will now show that the following conditions are equivalent:
ρ-epi : ∀ {X} → Epi (ρ {X}) ρ-epi : ∀ {X} → Epi (ρ {X})
ρ-epi {X} = Coequalizer⇒Epi (coeqs X) ρ-epi {X} = Coequalizer⇒Epi (coeqs X)
-- TODO this belongs in a different module
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ˡ
ρ▷ : ∀ {X} → ρ ∘ ▷ ≈ ρ {X} ρ▷ : ∀ {X} → ρ ∘ ▷ ≈ ρ {X}
ρ▷ {X} = sym (begin ρ▷ {X} = sym (begin
ρ ≈⟨ introʳ intro-helper ⟩ ρ ≈⟨ introʳ intro-helper ⟩

112
src/Monad/Instance/Delay/Strong.lagda.md
View file

@ -38,7 +38,60 @@ module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : De
open Monad monad using (η; μ) open Monad monad using (η; μ)
-- TODO change 'coinduction' proofs, move the two proofs i.e. f ≈ ! and ! ≈ g to the where clause -- TODO change 'coinduction' proofs, move the two proofs i.e. f ≈ ! and ! ≈ g to the where clause
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ˡ))
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ˡ⁻¹ ∎)
module τ-mod (P : Category.Obj (CProduct C C)) where
private
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 }))
open τ-mod
strength : Strength monoidal monad strength : Strength monoidal monad
strength = record strength = record
{ strengthen = ntHelper (record { strengthen = ntHelper (record
@ -56,58 +109,6 @@ module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : De
; strength-assoc = strength-assoc' -- square ; strength-assoc = strength-assoc' -- square
} }
where 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 : Obj} → extend (now ∘ π₂) ∘ τ (Terminal.⊤ terminal , X) ≈ π₂
identityˡ' {X} = begin 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 extend (now ∘ π₂) ∘ τ _ ≈⟨ sym (Terminal.!-unique (coalgebras X) {A = record { A = Terminal.⊤ terminal × D₀ X ; α = (π₂ +₁ idC) ∘ distributeˡ⁻¹ ∘ (idC ⁂ out) }} (record { f = extend (now ∘ π₂) ∘ τ _ ; commutes = begin
@ -141,13 +142,6 @@ module Monad.Instance.Delay.Strong {o ℓ e} (ambient : Ambient o ℓ e) (D : De
diag₂ = τ-law diag₂ = τ-law
diag₃ : out {X} ∘ extend (now ∘ π₂ {A = Terminal.⊤ terminal} {B = X}) ≈ (π₂ +₁ extend (now ∘ π₂)) ∘ out diag₃ : out {X} ∘ extend (now ∘ π₂ {A = Terminal.⊤ terminal} {B = X}) ≈ (π₂ +₁ extend (now ∘ π₂)) ∘ out
diag₃ = out-law π₂ 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} → extend idC ∘ (extend (now ∘ τ _)) ∘ τ _ ≈ τ (X , Y) ∘ (idC ⁂ extend idC)
μ-η-comm' {X} {Y} = begin μ-η-comm' {X} {Y} = begin