From ed46536d09c9045806403a3230e360dc6649037b Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Sun, 22 Oct 2023 17:22:27 +0200 Subject: [PATCH 01/15] Added right strength --- src/Categories/Monad/Strong.agda | 40 ++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/src/Categories/Monad/Strong.agda b/src/Categories/Monad/Strong.agda index 95dbd0bb3..8dddab05a 100644 --- a/src/Categories/Monad/Strong.agda +++ b/src/Categories/Monad/Strong.agda @@ -22,6 +22,8 @@ private variable o ℓ e : Level +-- (left) strength on a monad + record Strength {C : Category o ℓ e} (V : Monoidal C) (M : Monad C) : Set (o ⊔ ℓ ⊔ e) where open Category C open Monoidal V @@ -57,3 +59,41 @@ record StrongMonad {C : Category o ℓ e} (V : Monoidal C) : Set (o ⊔ ℓ ⊔ module M = Monad M open Strength strength public + +-- right strength + +record RightStrength {C : Category o ℓ e} (V : Monoidal C) (M : Monad C) : Set (o ⊔ ℓ ⊔ e) where + open Category C + open Monoidal V + private + module M = Monad M + open M using (F) + open NaturalTransformation M.η using (η) + open NaturalTransformation M.μ renaming (η to μ) + open Functor F + field + strengthen : NaturalTransformation (⊗ ∘F (F ⁂ idF)) (F ∘F ⊗) + + module strengthen = NaturalTransformation strengthen + private + module u = strengthen + + field + -- strengthening with 1 is irrelevant + identityˡ : {A : Obj} → F₁ (unitorʳ.from) ∘ u.η (A , unit) ≈ unitorʳ.from + -- commutes with unit (of monad) + η-comm : {A B : Obj} → u.η (A , B) ∘ (η A ⊗₁ id) ≈ η (A ⊗₀ B) + -- strength commutes with multiplication + μ-η-comm : {A B : Obj} → μ (A ⊗₀ B) ∘ F₁ (u.η (A , B)) ∘ u.η (F₀ A , B) + ≈ u.η (A , B) ∘ μ A ⊗₁ id + -- consecutive applications of strength commute (i.e. strength is associative) + strength-assoc : {A B C : Obj} → F₁ associator.to ∘ u.η (A , B ⊗₀ C) + ≈ u.η (A ⊗₀ B , C) ∘ u.η (A , B) ⊗₁ id ∘ associator.to + +record RightStrongMonad {C : Category o ℓ e} (V : Monoidal C) : Set (o ⊔ ℓ ⊔ e) where + field + M : Monad C + rightStrength : RightStrength V M + + module M = Monad M + open RightStrength rightStrength public \ No newline at end of file From 7e741af38e55bf3f11ebf7fa4094b6763fcb025c Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Sun, 22 Oct 2023 18:45:55 +0200 Subject: [PATCH 02/15] started working on proof --- src/Categories/Monad/Commutative.agda | 34 +++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 src/Categories/Monad/Commutative.agda diff --git a/src/Categories/Monad/Commutative.agda b/src/Categories/Monad/Commutative.agda new file mode 100644 index 000000000..b56a4f49d --- /dev/null +++ b/src/Categories/Monad/Commutative.agda @@ -0,0 +1,34 @@ +{-# OPTIONS --without-K --safe #-} + +-- Commutative Monad on a symmetric monoidal category +-- https://ncatlab.org/nlab/show/commutative+monad + +module Categories.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 + + + σ : ∀ {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.₁ σ ∘ τ \ No newline at end of file From 0256ad9e9065136bd64501de2a85a51d59668c2c Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Mon, 23 Oct 2023 16:24:25 +0200 Subject: [PATCH 03/15] Started proof --- src/Categories/Monad/Strong/Properties.agda | 109 ++++++++++++++++++++ 1 file changed, 109 insertions(+) create mode 100644 src/Categories/Monad/Strong/Properties.agda diff --git a/src/Categories/Monad/Strong/Properties.agda b/src/Categories/Monad/Strong/Properties.agda new file mode 100644 index 000000000..8c3d65431 --- /dev/null +++ b/src/Categories/Monad/Strong/Properties.agda @@ -0,0 +1,109 @@ +{-# OPTIONS --without-K --safe #-} + +-- In symmetric monoidal categories left and right strength imply each other + +module Categories.Monad.Strong.Properties where + +open import Level +open import Data.Product using (_,_; _×_) + +open import Categories.Category +open import Categories.Category.Product +open import Categories.Functor renaming (id to idF) +open import Categories.Category.Monoidal +open import Categories.Category.Monoidal.Symmetric +open import Categories.NaturalTransformation hiding (id) +open import Categories.Monad +open import Categories.Monad.Strong + +import Categories.Morphism.Reasoning as MR + +private + variable + o ℓ e : Level + +module _ {C : Category o ℓ e} (V : Monoidal C) (S : Symmetric V) where + open Category C + -- open Monoidal V + open Symmetric S + open import Categories.Category.Monoidal.Braided.Properties braided + open HomReasoning + open Equiv + open MR C + + Strength⇒RightStrength : ∀ {M : Monad C} → Strength V M → RightStrength V M + Strength⇒RightStrength {M} strength = record + { strengthen = ntHelper (record + { η = η' + ; commute = commute' + }) + ; identityˡ = identityˡ' + ; η-comm = η-comm' + ; μ-η-comm = μ-η-comm' + ; strength-assoc = strength-assoc' + } + where + open Monad M using (F; μ; η) + -- open Strength strength + module strength = Strength strength + module t = strength.strengthen + -- TODO use ⇒ for both + η' : ∀ ((X , Y) : Obj × Obj) → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) + η' (X , Y) = F.₁ (braiding.⇐.η (X , Y)) ∘ t.η (Y , X) ∘ braiding.⇒.η (F.₀ X , Y) + commute' : ∀ {(X , Y) (U , V) : Obj × Obj} ((f , g) : Product C C [ (X , Y) , (U , V) ]) → η' (U , V) ∘ (F.₁ f ⊗₁ g) ≈ F.₁ (f ⊗₁ g) ∘ η' (X , Y) + commute' {X , Y} {U , V} (f , g) = begin + (F.₁ (braiding.⇐.η (U , V)) ∘ t.η (V , U) ∘ braiding.⇒.η (F.₀ U , V)) ∘ (F.₁ f ⊗₁ g) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (F.₁ f , g))) ⟩ + F.₁ (braiding.⇐.η (U , V)) ∘ t.η (V , U) ∘ ((g ⊗₁ F.₁ f) ∘ braiding.⇒.η (F.₀ X , Y)) ≈⟨ refl⟩∘⟨ pullˡ (t.commute (g , f)) ⟩ + F.₁ (braiding.⇐.η (U , V)) ∘ ((F.₁ (g ⊗₁ f) ∘ t.η (Y , X)) ∘ braiding.⇒.η (F.₀ X , Y)) ≈⟨ pullˡ (pullˡ (sym F.homomorphism)) ⟩ + (F.₁ (braiding.⇐.η (U , V) ∘ (g ⊗₁ f)) ∘ t.η (Y , X)) ∘ braiding.⇒.η (F.₀ X , Y) ≈⟨ F.F-resp-≈ (braiding.⇐.commute (f , g)) ⟩∘⟨refl ⟩∘⟨refl ⟩ + (F.₁ ((f ⊗₁ g) ∘ braiding.⇐.η (X , Y)) ∘ t.η (Y , X)) ∘ braiding.⇒.η (F.₀ X , Y) ≈⟨ pushˡ F.homomorphism ⟩∘⟨refl ⟩ + (F.₁ (f ⊗₁ g) ∘ F.₁ (braiding.⇐.η (X , Y)) ∘ t.η (Y , X)) ∘ braiding.⇒.η (F.₀ X , Y) ≈⟨ assoc²' ⟩ + (F.₁ (f ⊗₁ g) ∘ η' (X , Y)) ∎ + identityˡ' : ∀ {A : Obj} → F.₁ unitorʳ.from ∘ η' (A , unit) ≈ unitorʳ.from + identityˡ' {A} = begin + F.₁ unitorʳ.from ∘ F.₁ (braiding.⇐.η (A , unit)) ∘ t.η (unit , A) ∘ braiding.⇒.η (F.₀ A , unit) ≈⟨ pullˡ (sym F.homomorphism) ⟩ + F.₁ (unitorʳ.from ∘ braiding.⇐.η (A , unit)) ∘ t.η (unit , A) ∘ braiding.⇒.η (F.₀ A , unit) ≈⟨ ((F.F-resp-≈ inv-braiding-coherence) ⟩∘⟨refl) ⟩ + F.₁ unitorˡ.from ∘ t.η (unit , A) ∘ braiding.⇒.η (F.₀ A , unit) ≈⟨ pullˡ strength.identityˡ ⟩ + unitorˡ.from ∘ braiding.⇒.η (F.₀ A , unit) ≈⟨ braiding-coherence ⟩ + unitorʳ.from ∎ + η-comm' : ∀ {A B : Obj} → η' (A , B) ∘ η.η A ⊗₁ id ≈ η.η (A ⊗₀ B) + η-comm' {A} {B} = begin + (F.₁ (braiding.⇐.η (A , B)) ∘ t.η (B , A) ∘ braiding.⇒.η (F.₀ A , B)) ∘ (η.η A ⊗₁ id) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (η.η A , id))) ⟩ + F.₁ (braiding.⇐.η (A , B)) ∘ t.η (B , A) ∘ ((id ⊗₁ η.η A) ∘ braiding.⇒.η (A , B)) ≈⟨ (refl⟩∘⟨ (pullˡ strength.η-comm)) ⟩ + F.₁ (braiding.⇐.η (A , B)) ∘ η.η (B ⊗₀ A) ∘ braiding.⇒.η (A , B) ≈⟨ pullˡ (sym (η.commute (braiding.⇐.η (A , B)))) ⟩ + (η.η (A ⊗₀ B) ∘ braiding.⇐.η (A , B)) ∘ braiding.⇒.η (A , B) ≈⟨ cancelʳ (braiding.iso.isoˡ (A , B)) ⟩ + η.η (A ⊗₀ B) ∎ + μ-η-comm' : ∀ {A B : Obj} → μ.η (A ⊗₀ B) ∘ F.₁ (η' (A , B)) ∘ η' (F.₀ A , B) ≈ η' (A , B) ∘ μ.η A ⊗₁ id + μ-η-comm' {A} {B} = begin + μ.η (A ⊗₀ B) ∘ F.F₁ (η' (A , B)) ∘ F.₁ (braiding.⇐.η (F.₀ A , B)) ∘ t.η (B , F.₀ A) ∘ braiding.⇒.η (F.₀ (F.₀ A) , B) ≈⟨ (refl⟩∘⟨ (pullˡ (sym F.homomorphism))) ⟩ + μ.η (A ⊗₀ B) ∘ F.₁ (η' (A , B) ∘ braiding.⇐.η (F.₀ A , B)) ∘ t.η (B , F.₀ A) ∘ braiding.⇒.η (F.₀ (F.₀ A) , B) ≈⟨ (refl⟩∘⟨ ((F.F-resp-≈ (pullʳ (cancelʳ (braiding.iso.isoʳ (F.₀ A , B))))) ⟩∘⟨refl)) ⟩ + μ.η (A ⊗₀ B) ∘ F.₁ (F.₁ (braiding.⇐.η (A , B)) ∘ t.η (B , A)) ∘ t.η (B , F.₀ A) ∘ braiding.⇒.η (F.₀ (F.₀ A) , B) ≈⟨ (refl⟩∘⟨ (F.homomorphism ⟩∘⟨refl)) ⟩ + μ.η (A ⊗₀ B) ∘ (F.₁ (F.₁ (braiding.⇐.η (A , B))) ∘ F.₁ (t.η (B , A))) ∘ t.η (B , F.₀ A) ∘ braiding.⇒.η (F.₀ (F.₀ A) , B) ≈⟨ pullˡ (pullˡ (μ.commute (braiding.⇐.η (A , B)))) ⟩ + ((F.₁ (braiding.⇐.η (A , B)) ∘ μ.η (B ⊗₀ A)) ∘ F.₁ (t.η (B , A))) ∘ t.η (B , F.₀ A) ∘ braiding.⇒.η (F.₀ (F.₀ A) , B) ≈⟨ (assoc² ○ (refl⟩∘⟨ sym assoc²')) ⟩ + F.₁ (braiding.⇐.η (A , B)) ∘ (μ.η (B ⊗₀ A) ∘ F.₁ (t.η (B , A)) ∘ t.η (B , F.₀ A)) ∘ braiding.⇒.η ((F.₀ (F.₀ A)) , B) ≈⟨ refl⟩∘⟨ pushˡ strength.μ-η-comm ⟩ + F.₁ (braiding.⇐.η (A , B)) ∘ t.η (B , A) ∘ (id ⊗₁ μ.η A) ∘ braiding.⇒.η ((F.₀ (F.₀ A)) , B) ≈˘⟨ pullʳ (pullʳ (braiding.⇒.commute (μ.η A , id))) ⟩ + η' (A , B) ∘ μ.η A ⊗₁ id ∎ + strength-assoc' : {X Y Z : Obj} → F.₁ associator.to ∘ η' (X , Y ⊗₀ Z) ≈ η' (X ⊗₀ Y , Z) ∘ η' (X , Y) ⊗₁ id ∘ associator.to + strength-assoc' {X} {Y} {Z} = begin + F.₁ associator.to ∘ F.₁ (braiding.⇐.η (X , Y ⊗₀ Z)) ∘ t.η (Y ⊗₀ Z , X) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ≈⟨ pullˡ (sym F.homomorphism) ⟩ + F.₁ (associator.to ∘ braiding.⇐.η (X , Y ⊗₀ Z)) ∘ t.η (Y ⊗₀ Z , X) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ≈⟨ {! !} ⟩ + F.₁ ((associator.to ∘ braiding.⇐.η (X , Y ⊗₀ Z)) ∘ associator.to ∘ associator.from) ∘ t.η (Y ⊗₀ Z , X) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ≈⟨ {! !} ⟩ + F.₁ (((braiding.⇒.η (Y , X) ⊗₁ id) ∘ associator.to ∘ (id ⊗₁ braiding.⇒.η (Z , X))) ∘ associator.from) ∘ t.η (Y ⊗₀ Z , X) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + F.₁ (braiding.⇒.η (Y , X) ⊗₁ id) ∘ F.₁ associator.to ∘ F.₁ (id ⊗₁ braiding.⇒.η (Z , X)) ∘ F.₁ associator.from ∘ t.η (Y ⊗₀ Z , X) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ≈⟨ {! !} ⟩ + F.₁ (braiding.⇒.η (Y , X) ⊗₁ id) ∘ F.₁ associator.to ∘ F.₁ (id ⊗₁ braiding.⇒.η (Z , X)) ∘ (t.η (Y , Z ⊗₀ X) ∘ (id ⊗₁ t.η (Z , X)) ∘ associator.from) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ pullˡ (pullˡ (sym (t.commute (id , braiding.⇒.η (Z , X)))))) ⟩ + F.₁ (braiding.⇒.η (Y , X) ⊗₁ id) ∘ F.₁ associator.to ∘ ((t.η (Y , (X ⊗₀ Z)) ∘ (id ⊗₁ F.₁ (braiding.⇒.η (Z , X)))) ∘ ((id ⊗₁ t.η (Z , X)) ∘ associator.from)) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ≈⟨ {! !} ⟩ + (F.₁ (braiding.⇒.η (Y , X) ⊗₁ id) ∘ F.₁ associator.to ∘ ((t.η (Y , (X ⊗₀ Z)) ∘ (id ⊗₁ F.₁ (braiding.⇒.η (Z , X)))) ∘ ((id ⊗₁ t.η (Z , X)) ∘ associator.from)) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z)) ∘ associator.from ∘ associator.to ≈⟨ pullʳ (pullʳ (pullˡ assoc²)) ⟩ + F.₁ (braiding.⇒.η (Y , X) ⊗₁ id) ∘ F.₁ associator.to ∘ (((t.η (Y , X ⊗₀ Z) ∘ (id ⊗₁ F.₁ (braiding.⇒.η (Z , X)))) ∘ (id ⊗₁ t.η (Z , X) ∘ associator.from) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ∘ associator.from) ∘ associator.to) ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ (pullʳ (refl⟩∘⟨ pullʳ (sym hexagon₁)) ⟩∘⟨refl)) ⟩ + F.₁ (braiding.⇒.η (Y , X) ⊗₁ id) ∘ F.₁ associator.to ∘ (t.η (Y , X ⊗₀ Z) ∘ (id ⊗₁ F.₁ (braiding.⇒.η (Z , X))) ∘ (id ⊗₁ t.η (Z , X)) ∘ (id ⊗₁ braiding.⇒.η (F.₀ X , Z)) ∘ associator.from ∘ (braiding.⇒.η (F.₀ X , Y) ⊗₁ id)) ∘ associator.to ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + (F.₁ (braiding.⇒.η (Y , X) ⊗₁ id) ∘ F.₁ associator.to ∘ (t.η (Y , X ⊗₀ Z) ∘ (id ⊗₁ η' (X , Z)) ∘ associator.from ∘ (braiding.⇒.η (F.₀ X , Y) ⊗₁ id)) ∘ associator.to) ≈⟨ {! t.commute !} ⟩ + {! !} ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + {! !} ≈˘⟨ {! !} ⟩ + ((F.₁ (braiding.⇐.η (X ⊗₀ Y , Z)) ∘ t.η (Z , X ⊗₀ Y)) ∘ ((id ⊗₁ η' (X , Y)) ∘ braiding.⇒.η (F.₀ X ⊗₀ Y , Z)) ∘ associator.to) ≈˘⟨ {! !} ⟩ + (F.₁ (braiding.⇐.η (X ⊗₀ Y , Z)) ∘ t.η (Z , X ⊗₀ Y) ∘ braiding.⇒.η (F.₀ (X ⊗₀ Y) , Z)) ∘ (η' (X , Y) ⊗₁ id) ∘ associator.to ∎ + where + braiding-eq : ∀ {X Y} → braiding.⇐.η (X , Y) ≈ braiding.⇒.η (Y , X) + braiding-eq = introʳ commutative ○ cancelˡ (braiding.iso.isoˡ _) + \ No newline at end of file From 3a07c9e55335edd0095e6f37d1a64e48102203f3 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Fri, 3 Nov 2023 08:55:03 +0100 Subject: [PATCH 04/15] worked on assoc --- src/Categories/Monad/Strong.agda | 12 +++---- src/Categories/Monad/Strong/Properties.agda | 39 ++++++++++++--------- 2 files changed, 29 insertions(+), 22 deletions(-) diff --git a/src/Categories/Monad/Strong.agda b/src/Categories/Monad/Strong.agda index 8dddab05a..90ed6353c 100644 --- a/src/Categories/Monad/Strong.agda +++ b/src/Categories/Monad/Strong.agda @@ -44,13 +44,13 @@ record Strength {C : Category o ℓ e} (V : Monoidal C) (M : Monad C) : Set (o -- strengthening with 1 is irrelevant identityˡ : {A : Obj} → F₁ (unitorˡ.from) ∘ t.η (unit , A) ≈ unitorˡ.from -- commutes with unit (of monad) - η-comm : {A B : Obj} → t.η (A , B) ∘ (id ⊗₁ η B) ≈ η (A ⊗₀ B) + η-comm : {A B : Obj} → t.η (A , B) ∘ (id ⊗₁ η B) ≈ η (A ⊗₀ B) -- strength commutes with multiplication μ-η-comm : {A B : Obj} → μ (A ⊗₀ B) ∘ F₁ (t.η (A , B)) ∘ t.η (A , F₀ B) - ≈ t.η (A , B) ∘ id ⊗₁ μ B + ≈ t.η (A , B) ∘ (id ⊗₁ μ B) -- consecutive applications of strength commute (i.e. strength is associative) strength-assoc : {A B C : Obj} → F₁ associator.from ∘ t.η (A ⊗₀ B , C) - ≈ t.η (A , B ⊗₀ C) ∘ id ⊗₁ t.η (B , C) ∘ associator.from + ≈ t.η (A , B ⊗₀ C) ∘ (id ⊗₁ t.η (B , C)) ∘ associator.from record StrongMonad {C : Category o ℓ e} (V : Monoidal C) : Set (o ⊔ ℓ ⊔ e) where field @@ -82,13 +82,13 @@ record RightStrength {C : Category o ℓ e} (V : Monoidal C) (M : Monad C) : Set -- strengthening with 1 is irrelevant identityˡ : {A : Obj} → F₁ (unitorʳ.from) ∘ u.η (A , unit) ≈ unitorʳ.from -- commutes with unit (of monad) - η-comm : {A B : Obj} → u.η (A , B) ∘ (η A ⊗₁ id) ≈ η (A ⊗₀ B) + η-comm : {A B : Obj} → u.η (A , B) ∘ (η A ⊗₁ id) ≈ η (A ⊗₀ B) -- strength commutes with multiplication μ-η-comm : {A B : Obj} → μ (A ⊗₀ B) ∘ F₁ (u.η (A , B)) ∘ u.η (F₀ A , B) - ≈ u.η (A , B) ∘ μ A ⊗₁ id + ≈ u.η (A , B) ∘ (μ A ⊗₁ id) -- consecutive applications of strength commute (i.e. strength is associative) strength-assoc : {A B C : Obj} → F₁ associator.to ∘ u.η (A , B ⊗₀ C) - ≈ u.η (A ⊗₀ B , C) ∘ u.η (A , B) ⊗₁ id ∘ associator.to + ≈ u.η (A ⊗₀ B , C) ∘ (u.η (A , B) ⊗₁ id) ∘ associator.to record RightStrongMonad {C : Category o ℓ e} (V : Monoidal C) : Set (o ⊔ ℓ ⊔ e) where field diff --git a/src/Categories/Monad/Strong/Properties.agda b/src/Categories/Monad/Strong/Properties.agda index 8c3d65431..befcfe046 100644 --- a/src/Categories/Monad/Strong/Properties.agda +++ b/src/Categories/Monad/Strong/Properties.agda @@ -85,25 +85,32 @@ module _ {C : Category o ℓ e} (V : Monoidal C) (S : Symmetric V) where η' (A , B) ∘ μ.η A ⊗₁ id ∎ strength-assoc' : {X Y Z : Obj} → F.₁ associator.to ∘ η' (X , Y ⊗₀ Z) ≈ η' (X ⊗₀ Y , Z) ∘ η' (X , Y) ⊗₁ id ∘ associator.to strength-assoc' {X} {Y} {Z} = begin - F.₁ associator.to ∘ F.₁ (braiding.⇐.η (X , Y ⊗₀ Z)) ∘ t.η (Y ⊗₀ Z , X) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ≈⟨ pullˡ (sym F.homomorphism) ⟩ - F.₁ (associator.to ∘ braiding.⇐.η (X , Y ⊗₀ Z)) ∘ t.η (Y ⊗₀ Z , X) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ≈⟨ {! !} ⟩ - F.₁ ((associator.to ∘ braiding.⇐.η (X , Y ⊗₀ Z)) ∘ associator.to ∘ associator.from) ∘ t.η (Y ⊗₀ Z , X) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ≈⟨ {! !} ⟩ - F.₁ (((braiding.⇒.η (Y , X) ⊗₁ id) ∘ associator.to ∘ (id ⊗₁ braiding.⇒.η (Z , X))) ∘ associator.from) ∘ t.η (Y ⊗₀ Z , X) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ≈⟨ {! !} ⟩ + F.₁ α ∘ F.₁ (braiding.⇐.η (X , Y ⊗₀ Z)) ∘ t.η (Y ⊗₀ Z , X) ∘ B ≈⟨ {! !} ⟩ + (F.₁ α ∘ F.₁ B ∘ τ ∘ B) ≈⟨ {! !} ⟩ {! !} ≈⟨ {! !} ⟩ - F.₁ (braiding.⇒.η (Y , X) ⊗₁ id) ∘ F.₁ associator.to ∘ F.₁ (id ⊗₁ braiding.⇒.η (Z , X)) ∘ F.₁ associator.from ∘ t.η (Y ⊗₀ Z , X) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ≈⟨ {! !} ⟩ - F.₁ (braiding.⇒.η (Y , X) ⊗₁ id) ∘ F.₁ associator.to ∘ F.₁ (id ⊗₁ braiding.⇒.η (Z , X)) ∘ (t.η (Y , Z ⊗₀ X) ∘ (id ⊗₁ t.η (Z , X)) ∘ associator.from) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ pullˡ (pullˡ (sym (t.commute (id , braiding.⇒.η (Z , X)))))) ⟩ - F.₁ (braiding.⇒.η (Y , X) ⊗₁ id) ∘ F.₁ associator.to ∘ ((t.η (Y , (X ⊗₀ Z)) ∘ (id ⊗₁ F.₁ (braiding.⇒.η (Z , X)))) ∘ ((id ⊗₁ t.η (Z , X)) ∘ associator.from)) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ≈⟨ {! !} ⟩ - (F.₁ (braiding.⇒.η (Y , X) ⊗₁ id) ∘ F.₁ associator.to ∘ ((t.η (Y , (X ⊗₀ Z)) ∘ (id ⊗₁ F.₁ (braiding.⇒.η (Z , X)))) ∘ ((id ⊗₁ t.η (Z , X)) ∘ associator.from)) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z)) ∘ associator.from ∘ associator.to ≈⟨ pullʳ (pullʳ (pullˡ assoc²)) ⟩ - F.₁ (braiding.⇒.η (Y , X) ⊗₁ id) ∘ F.₁ associator.to ∘ (((t.η (Y , X ⊗₀ Z) ∘ (id ⊗₁ F.₁ (braiding.⇒.η (Z , X)))) ∘ (id ⊗₁ t.η (Z , X) ∘ associator.from) ∘ braiding.⇒.η (F.₀ X , Y ⊗₀ Z) ∘ associator.from) ∘ associator.to) ≈⟨ (refl⟩∘⟨ refl⟩∘⟨ (pullʳ (refl⟩∘⟨ pullʳ (sym hexagon₁)) ⟩∘⟨refl)) ⟩ - F.₁ (braiding.⇒.η (Y , X) ⊗₁ id) ∘ F.₁ associator.to ∘ (t.η (Y , X ⊗₀ Z) ∘ (id ⊗₁ F.₁ (braiding.⇒.η (Z , X))) ∘ (id ⊗₁ t.η (Z , X)) ∘ (id ⊗₁ braiding.⇒.η (F.₀ X , Z)) ∘ associator.from ∘ (braiding.⇒.η (F.₀ X , Y) ⊗₁ id)) ∘ associator.to ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - (F.₁ (braiding.⇒.η (Y , X) ⊗₁ id) ∘ F.₁ associator.to ∘ (t.η (Y , X ⊗₀ Z) ∘ (id ⊗₁ η' (X , Z)) ∘ associator.from ∘ (braiding.⇒.η (F.₀ X , Y) ⊗₁ id)) ∘ associator.to) ≈⟨ {! t.commute !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈˘⟨ {! !} ⟩ - ((F.₁ (braiding.⇐.η (X ⊗₀ Y , Z)) ∘ t.η (Z , X ⊗₀ Y)) ∘ ((id ⊗₁ η' (X , Y)) ∘ braiding.⇒.η (F.₀ X ⊗₀ Y , Z)) ∘ associator.to) ≈˘⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + {! !} ≈⟨ {! !} ⟩ + -- TODO check what id × B ∘ B ∘ α corresponds to, maybe i can rewrite it somehow + F.₁ B ∘ F.₁ (id ⊗₁ B) ∘ ((F.₁ α⁻¹ ∘ τ) ∘ α) ∘ (id ⊗₁ B) ∘ B ∘ α ≈⟨ {! !} ⟩ + F.₁ B ∘ F.₁ (id ⊗₁ B) ∘ τ ∘ (id ⊗₁ τ) ∘ (α⁻¹ ∘ α) ∘ (id ⊗₁ B) ∘ B ∘ α ≈⟨ {! !} ⟩ -- all steps below work + F.₁ B ∘ F.₁ (id ⊗₁ B) ∘ τ ∘ (id ⊗₁ τ) ∘ (id ⊗₁ B) ∘ B ∘ α ≈⟨ {! !} ⟩ + F.₁ B ∘ (F.₁ (id ⊗₁ B) ∘ τ ∘ ((id ⊗₁ τ) ∘ (id ⊗₁ B)) ∘ B) ∘ α ≈⟨ {! !} ⟩ + F.₁ B ∘ (F.₁ (id ⊗₁ B) ∘ τ ∘ (id ⊗₁ (τ ∘ B)) ∘ B) ∘ α ≈⟨ {! !} ⟩ + F.₁ B ∘ τ ∘ ((id ⊗₁ F.₁ B) ∘ (id ⊗₁ (τ ∘ B)) ∘ B) ∘ α ≈⟨ {! !} ⟩ + F.₁ B ∘ τ ∘ ((id ⊗₁ (F.₁ B ∘ τ ∘ B)) ∘ B) ∘ α ≈⟨ {! !} ⟩ -- B swap + (F.₁ B ∘ τ ∘ B) ∘ (σ ⊗₁ id) ∘ α ≈⟨ {! !} ⟩ (F.₁ (braiding.⇐.η (X ⊗₀ Y , Z)) ∘ t.η (Z , X ⊗₀ Y) ∘ braiding.⇒.η (F.₀ (X ⊗₀ Y) , Z)) ∘ (η' (X , Y) ⊗₁ id) ∘ associator.to ∎ where + α = associator.to + α⁻¹ = associator.from + B : ∀ {X Y} → X ⊗₀ Y ⇒ Y ⊗₀ X + B {X} {Y} = braiding.⇒.η (X , Y) + τ : ∀ {X Y} → X ⊗₀ F.₀ Y ⇒ F.₀ (X ⊗₀ Y) + τ {X} {Y} = t.η (X , Y) + σ : ∀ {X Y} → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) + σ {X} {Y} = η' (X , Y) + -- strength.strength-assoc : F.₁ α⁻¹ ∘ τ ≈ τ ∘ (id × τ) ∘ α⁻¹ braiding-eq : ∀ {X Y} → braiding.⇐.η (X , Y) ≈ braiding.⇒.η (Y , X) braiding-eq = introʳ commutative ○ cancelˡ (braiding.iso.isoˡ _) \ No newline at end of file From 41a455895fc2bbf471f13c96ae8af39998162737 Mon Sep 17 00:00:00 2001 From: Leon Vatthauer Date: Thu, 7 Dec 2023 18:30:24 +0100 Subject: [PATCH 05/15] tidy up --- src/Categories/Monad/Commutative.agda | 53 +++++--- src/Categories/Monad/Strong/Properties.agda | 141 +++++++++----------- 2 files changed, 99 insertions(+), 95 deletions(-) diff --git a/src/Categories/Monad/Commutative.agda b/src/Categories/Monad/Commutative.agda index b56a4f49d..c7fb3b4f8 100644 --- a/src/Categories/Monad/Commutative.agda +++ b/src/Categories/Monad/Commutative.agda @@ -8,27 +8,42 @@ module Categories.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 +open import Categories.Category.Core using (Category) +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Symmetric using (Symmetric) +open import Categories.Monad using (Monad) +open import Categories.Monad.Strong using (StrongMonad; RightStrength; Strength) +open import Categories.Monad.Strong.Properties using (Strength⇒RightStrength) 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 - - - σ : ∀ {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.₁ σ ∘ τ \ No newline at end of file +module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where + record Commutative (LSM : StrongMonad V) : Set (o ⊔ ℓ ⊔ e) where + open Category C + open Symmetric S + open StrongMonad LSM + + rightStrength : RightStrength V M + rightStrength = Strength⇒RightStrength S strength + + private + module LS = Strength strength + module RS = RightStrength rightStrength + σ : ∀ {X Y} → X ⊗₀ M.F.₀ Y ⇒ M.F.₀ (X ⊗₀ Y) + σ {X} {Y} = LS.strengthen.η (X , Y) + τ : ∀ {X Y} → M.F.₀ X ⊗₀ Y ⇒ M.F.₀ (X ⊗₀ Y) + τ {X} {Y} = RS.strengthen.η (X , Y) + + field + commutes : ∀ {X Y} → M.μ.η (X ⊗₀ Y) ∘ M.F.₁ τ ∘ σ ≈ M.μ.η (X ⊗₀ Y) ∘ M.F.₁ σ ∘ τ + + record CommutativeMonad : Set (o ⊔ ℓ ⊔ e) where + field + strongMonad : StrongMonad V + commutative : Commutative strongMonad + + open StrongMonad strongMonad public + open Commutative commutative public + \ No newline at end of file diff --git a/src/Categories/Monad/Strong/Properties.agda b/src/Categories/Monad/Strong/Properties.agda index befcfe046..427d5796d 100644 --- a/src/Categories/Monad/Strong/Properties.agda +++ b/src/Categories/Monad/Strong/Properties.agda @@ -7,14 +7,14 @@ module Categories.Monad.Strong.Properties where open import Level open import Data.Product using (_,_; _×_) -open import Categories.Category +open import Categories.Category.Core open import Categories.Category.Product open import Categories.Functor renaming (id to idF) -open import Categories.Category.Monoidal -open import Categories.Category.Monoidal.Symmetric -open import Categories.NaturalTransformation hiding (id) -open import Categories.Monad -open import Categories.Monad.Strong +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Symmetric using (Symmetric) +open import Categories.NaturalTransformation using (ntHelper) +open import Categories.Monad using (Monad) +open import Categories.Monad.Strong using (Strength; RightStrength; StrongMonad; RightStrongMonad) import Categories.Morphism.Reasoning as MR @@ -22,9 +22,8 @@ private variable o ℓ e : Level -module _ {C : Category o ℓ e} (V : Monoidal C) (S : Symmetric V) where +module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where open Category C - -- open Monoidal V open Symmetric S open import Categories.Category.Monoidal.Braided.Properties braided open HomReasoning @@ -34,8 +33,8 @@ module _ {C : Category o ℓ e} (V : Monoidal C) (S : Symmetric V) where Strength⇒RightStrength : ∀ {M : Monad C} → Strength V M → RightStrength V M Strength⇒RightStrength {M} strength = record { strengthen = ntHelper (record - { η = η' - ; commute = commute' + { η = τ + ; commute = λ (f , g) → commute' f g }) ; identityˡ = identityˡ' ; η-comm = η-comm' @@ -44,73 +43,63 @@ module _ {C : Category o ℓ e} (V : Monoidal C) (S : Symmetric V) where } where open Monad M using (F; μ; η) - -- open Strength strength module strength = Strength strength module t = strength.strengthen - -- TODO use ⇒ for both - η' : ∀ ((X , Y) : Obj × Obj) → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) - η' (X , Y) = F.₁ (braiding.⇐.η (X , Y)) ∘ t.η (Y , X) ∘ braiding.⇒.η (F.₀ X , Y) - commute' : ∀ {(X , Y) (U , V) : Obj × Obj} ((f , g) : Product C C [ (X , Y) , (U , V) ]) → η' (U , V) ∘ (F.₁ f ⊗₁ g) ≈ F.₁ (f ⊗₁ g) ∘ η' (X , Y) - commute' {X , Y} {U , V} (f , g) = begin - (F.₁ (braiding.⇐.η (U , V)) ∘ t.η (V , U) ∘ braiding.⇒.η (F.₀ U , V)) ∘ (F.₁ f ⊗₁ g) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (F.₁ f , g))) ⟩ - F.₁ (braiding.⇐.η (U , V)) ∘ t.η (V , U) ∘ ((g ⊗₁ F.₁ f) ∘ braiding.⇒.η (F.₀ X , Y)) ≈⟨ refl⟩∘⟨ pullˡ (t.commute (g , f)) ⟩ - F.₁ (braiding.⇐.η (U , V)) ∘ ((F.₁ (g ⊗₁ f) ∘ t.η (Y , X)) ∘ braiding.⇒.η (F.₀ X , Y)) ≈⟨ pullˡ (pullˡ (sym F.homomorphism)) ⟩ - (F.₁ (braiding.⇐.η (U , V) ∘ (g ⊗₁ f)) ∘ t.η (Y , X)) ∘ braiding.⇒.η (F.₀ X , Y) ≈⟨ F.F-resp-≈ (braiding.⇐.commute (f , g)) ⟩∘⟨refl ⟩∘⟨refl ⟩ - (F.₁ ((f ⊗₁ g) ∘ braiding.⇐.η (X , Y)) ∘ t.η (Y , X)) ∘ braiding.⇒.η (F.₀ X , Y) ≈⟨ pushˡ F.homomorphism ⟩∘⟨refl ⟩ - (F.₁ (f ⊗₁ g) ∘ F.₁ (braiding.⇐.η (X , Y)) ∘ t.η (Y , X)) ∘ braiding.⇒.η (F.₀ X , Y) ≈⟨ assoc²' ⟩ - (F.₁ (f ⊗₁ g) ∘ η' (X , Y)) ∎ - identityˡ' : ∀ {A : Obj} → F.₁ unitorʳ.from ∘ η' (A , unit) ≈ unitorʳ.from - identityˡ' {A} = begin - F.₁ unitorʳ.from ∘ F.₁ (braiding.⇐.η (A , unit)) ∘ t.η (unit , A) ∘ braiding.⇒.η (F.₀ A , unit) ≈⟨ pullˡ (sym F.homomorphism) ⟩ - F.₁ (unitorʳ.from ∘ braiding.⇐.η (A , unit)) ∘ t.η (unit , A) ∘ braiding.⇒.η (F.₀ A , unit) ≈⟨ ((F.F-resp-≈ inv-braiding-coherence) ⟩∘⟨refl) ⟩ - F.₁ unitorˡ.from ∘ t.η (unit , A) ∘ braiding.⇒.η (F.₀ A , unit) ≈⟨ pullˡ strength.identityˡ ⟩ - unitorˡ.from ∘ braiding.⇒.η (F.₀ A , unit) ≈⟨ braiding-coherence ⟩ - unitorʳ.from ∎ - η-comm' : ∀ {A B : Obj} → η' (A , B) ∘ η.η A ⊗₁ id ≈ η.η (A ⊗₀ B) - η-comm' {A} {B} = begin - (F.₁ (braiding.⇐.η (A , B)) ∘ t.η (B , A) ∘ braiding.⇒.η (F.₀ A , B)) ∘ (η.η A ⊗₁ id) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (η.η A , id))) ⟩ - F.₁ (braiding.⇐.η (A , B)) ∘ t.η (B , A) ∘ ((id ⊗₁ η.η A) ∘ braiding.⇒.η (A , B)) ≈⟨ (refl⟩∘⟨ (pullˡ strength.η-comm)) ⟩ - F.₁ (braiding.⇐.η (A , B)) ∘ η.η (B ⊗₀ A) ∘ braiding.⇒.η (A , B) ≈⟨ pullˡ (sym (η.commute (braiding.⇐.η (A , B)))) ⟩ - (η.η (A ⊗₀ B) ∘ braiding.⇐.η (A , B)) ∘ braiding.⇒.η (A , B) ≈⟨ cancelʳ (braiding.iso.isoˡ (A , B)) ⟩ - η.η (A ⊗₀ B) ∎ - μ-η-comm' : ∀ {A B : Obj} → μ.η (A ⊗₀ B) ∘ F.₁ (η' (A , B)) ∘ η' (F.₀ A , B) ≈ η' (A , B) ∘ μ.η A ⊗₁ id - μ-η-comm' {A} {B} = begin - μ.η (A ⊗₀ B) ∘ F.F₁ (η' (A , B)) ∘ F.₁ (braiding.⇐.η (F.₀ A , B)) ∘ t.η (B , F.₀ A) ∘ braiding.⇒.η (F.₀ (F.₀ A) , B) ≈⟨ (refl⟩∘⟨ (pullˡ (sym F.homomorphism))) ⟩ - μ.η (A ⊗₀ B) ∘ F.₁ (η' (A , B) ∘ braiding.⇐.η (F.₀ A , B)) ∘ t.η (B , F.₀ A) ∘ braiding.⇒.η (F.₀ (F.₀ A) , B) ≈⟨ (refl⟩∘⟨ ((F.F-resp-≈ (pullʳ (cancelʳ (braiding.iso.isoʳ (F.₀ A , B))))) ⟩∘⟨refl)) ⟩ - μ.η (A ⊗₀ B) ∘ F.₁ (F.₁ (braiding.⇐.η (A , B)) ∘ t.η (B , A)) ∘ t.η (B , F.₀ A) ∘ braiding.⇒.η (F.₀ (F.₀ A) , B) ≈⟨ (refl⟩∘⟨ (F.homomorphism ⟩∘⟨refl)) ⟩ - μ.η (A ⊗₀ B) ∘ (F.₁ (F.₁ (braiding.⇐.η (A , B))) ∘ F.₁ (t.η (B , A))) ∘ t.η (B , F.₀ A) ∘ braiding.⇒.η (F.₀ (F.₀ A) , B) ≈⟨ pullˡ (pullˡ (μ.commute (braiding.⇐.η (A , B)))) ⟩ - ((F.₁ (braiding.⇐.η (A , B)) ∘ μ.η (B ⊗₀ A)) ∘ F.₁ (t.η (B , A))) ∘ t.η (B , F.₀ A) ∘ braiding.⇒.η (F.₀ (F.₀ A) , B) ≈⟨ (assoc² ○ (refl⟩∘⟨ sym assoc²')) ⟩ - F.₁ (braiding.⇐.η (A , B)) ∘ (μ.η (B ⊗₀ A) ∘ F.₁ (t.η (B , A)) ∘ t.η (B , F.₀ A)) ∘ braiding.⇒.η ((F.₀ (F.₀ A)) , B) ≈⟨ refl⟩∘⟨ pushˡ strength.μ-η-comm ⟩ - F.₁ (braiding.⇐.η (A , B)) ∘ t.η (B , A) ∘ (id ⊗₁ μ.η A) ∘ braiding.⇒.η ((F.₀ (F.₀ A)) , B) ≈˘⟨ pullʳ (pullʳ (braiding.⇒.commute (μ.η A , id))) ⟩ - η' (A , B) ∘ μ.η A ⊗₁ id ∎ - strength-assoc' : {X Y Z : Obj} → F.₁ associator.to ∘ η' (X , Y ⊗₀ Z) ≈ η' (X ⊗₀ Y , Z) ∘ η' (X , Y) ⊗₁ id ∘ associator.to + B = braiding.⇒.η + τ : ∀ ((X , Y) : Obj × Obj) → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) + τ (X , Y) = F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ B (F.₀ X , Y) + α = associator.to + α⁻¹ = associator.from + braiding-eq : ∀ {X Y} → braiding.⇐.η (X , Y) ≈ B (Y , X) + braiding-eq = introʳ commutative ○ cancelˡ (braiding.iso.isoˡ _) + commute' : ∀ {X Y U V : Obj} (f : X ⇒ U) (g : Y ⇒ V) → τ (U , V) ∘ (F.₁ f ⊗₁ g) ≈ F.₁ (f ⊗₁ g) ∘ τ (X , Y) + commute' {X} {Y} {U} {V} f g = begin + (F.₁ (B (V , U)) ∘ t.η (V , U) ∘ B (F.₀ U , V)) ∘ (F.₁ f ⊗₁ g) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (F.₁ f , g))) ⟩ + F.₁ (B (V , U)) ∘ t.η (V , U) ∘ ((g ⊗₁ F.₁ f) ∘ B (F.₀ X , Y)) ≈⟨ refl⟩∘⟨ pullˡ (t.commute (g , f)) ⟩ + F.₁ (B (V , U)) ∘ ((F.₁ (g ⊗₁ f) ∘ t.η (Y , X)) ∘ B (F.₀ X , Y)) ≈⟨ pullˡ (pullˡ (sym F.homomorphism)) ⟩ + (F.₁ (B (V , U) ∘ (g ⊗₁ f)) ∘ t.η (Y , X)) ∘ B (F.₀ X , Y) ≈⟨ F.F-resp-≈ (braiding.⇒.commute (g , f)) ⟩∘⟨refl ⟩∘⟨refl ⟩ + (F.₁ ((f ⊗₁ g) ∘ B (Y , X)) ∘ t.η (Y , X)) ∘ B (F.₀ X , Y) ≈⟨ pushˡ F.homomorphism ⟩∘⟨refl ⟩ + (F.₁ (f ⊗₁ g) ∘ F.₁ (B (Y , X)) ∘ t.η (Y , X)) ∘ B (F.₀ X , Y) ≈⟨ assoc²' ⟩ + (F.₁ (f ⊗₁ g) ∘ τ (X , Y)) ∎ + identityˡ' : ∀ {X : Obj} → F.₁ unitorʳ.from ∘ τ (X , unit) ≈ unitorʳ.from + identityˡ' {X} = begin + F.₁ unitorʳ.from ∘ F.₁ (B (unit , X)) ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ pullˡ (sym F.homomorphism) ⟩ + F.₁ (unitorʳ.from ∘ B (unit , X)) ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ ((F.F-resp-≈ ((refl⟩∘⟨ sym braiding-eq) ○ inv-braiding-coherence)) ⟩∘⟨refl) ⟩ + F.₁ unitorˡ.from ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ pullˡ strength.identityˡ ⟩ + unitorˡ.from ∘ B (F.₀ X , unit) ≈⟨ braiding-coherence ⟩ + unitorʳ.from ∎ + η-comm' : ∀ {X Y : Obj} → τ (X , Y) ∘ η.η X ⊗₁ id ≈ η.η (X ⊗₀ Y) + η-comm' {X} {Y} = begin + (F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ B (F.₀ X , Y)) ∘ (η.η X ⊗₁ id) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (η.η X , id))) ⟩ + F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ ((id ⊗₁ η.η X) ∘ B (X , Y)) ≈⟨ (refl⟩∘⟨ (pullˡ strength.η-comm)) ⟩ + F.₁ (B (Y , X)) ∘ η.η (Y ⊗₀ X) ∘ B (X , Y) ≈⟨ pullˡ (sym (η.commute (B (Y , X)))) ⟩ + (η.η (X ⊗₀ Y) ∘ B (Y , X)) ∘ B (X , Y) ≈⟨ cancelʳ commutative ⟩ + η.η (X ⊗₀ Y) ∎ + μ-η-comm' : ∀ {X Y : Obj} → μ.η (X ⊗₀ Y) ∘ F.₁ (τ (X , Y)) ∘ τ (F.₀ X , Y) ≈ τ (X , Y) ∘ μ.η X ⊗₁ id + μ-η-comm' {X} {Y} = begin + μ.η (X ⊗₀ Y) ∘ F.F₁ (τ (X , Y)) ∘ F.₁ (B (Y , F.₀ X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ (pullˡ (sym F.homomorphism))) ⟩ + μ.η (X ⊗₀ Y) ∘ F.₁ (τ (X , Y) ∘ B (Y , F.₀ X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ ((F.F-resp-≈ (pullʳ (cancelʳ commutative))) ⟩∘⟨refl)) ⟩ + μ.η (X ⊗₀ Y) ∘ F.₁ (F.₁ (B (Y , X)) ∘ t.η (Y , X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ (F.homomorphism ⟩∘⟨refl)) ⟩ + μ.η (X ⊗₀ Y) ∘ (F.₁ (F.₁ (B (Y , X))) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ pullˡ (pullˡ (μ.commute (B (Y , X)))) ⟩ + ((F.₁ (B (Y , X)) ∘ μ.η (Y ⊗₀ X)) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (assoc² ○ (refl⟩∘⟨ sym assoc²')) ⟩ + F.₁ (B (Y , X)) ∘ (μ.η (Y ⊗₀ X) ∘ F.₁ (t.η (Y , X)) ∘ t.η (Y , F.₀ X)) ∘ B ((F.₀ (F.₀ X)) , Y) ≈⟨ refl⟩∘⟨ pushˡ strength.μ-η-comm ⟩ + F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ (id ⊗₁ μ.η X) ∘ B ((F.₀ (F.₀ X)) , Y) ≈˘⟨ pullʳ (pullʳ (braiding.⇒.commute (μ.η X , id))) ⟩ + τ (X , Y) ∘ μ.η X ⊗₁ id ∎ + strength-assoc' : {X Y Z : Obj} → F.₁ associator.to ∘ τ (X , Y ⊗₀ Z) ≈ τ (X ⊗₀ Y , Z) ∘ τ (X , Y) ⊗₁ id ∘ associator.to strength-assoc' {X} {Y} {Z} = begin - F.₁ α ∘ F.₁ (braiding.⇐.η (X , Y ⊗₀ Z)) ∘ t.η (Y ⊗₀ Z , X) ∘ B ≈⟨ {! !} ⟩ - (F.₁ α ∘ F.₁ B ∘ τ ∘ B) ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - {! !} ≈⟨ {! !} ⟩ - -- TODO check what id × B ∘ B ∘ α corresponds to, maybe i can rewrite it somehow - F.₁ B ∘ F.₁ (id ⊗₁ B) ∘ ((F.₁ α⁻¹ ∘ τ) ∘ α) ∘ (id ⊗₁ B) ∘ B ∘ α ≈⟨ {! !} ⟩ - F.₁ B ∘ F.₁ (id ⊗₁ B) ∘ τ ∘ (id ⊗₁ τ) ∘ (α⁻¹ ∘ α) ∘ (id ⊗₁ B) ∘ B ∘ α ≈⟨ {! !} ⟩ -- all steps below work - F.₁ B ∘ F.₁ (id ⊗₁ B) ∘ τ ∘ (id ⊗₁ τ) ∘ (id ⊗₁ B) ∘ B ∘ α ≈⟨ {! !} ⟩ - F.₁ B ∘ (F.₁ (id ⊗₁ B) ∘ τ ∘ ((id ⊗₁ τ) ∘ (id ⊗₁ B)) ∘ B) ∘ α ≈⟨ {! !} ⟩ - F.₁ B ∘ (F.₁ (id ⊗₁ B) ∘ τ ∘ (id ⊗₁ (τ ∘ B)) ∘ B) ∘ α ≈⟨ {! !} ⟩ - F.₁ B ∘ τ ∘ ((id ⊗₁ F.₁ B) ∘ (id ⊗₁ (τ ∘ B)) ∘ B) ∘ α ≈⟨ {! !} ⟩ - F.₁ B ∘ τ ∘ ((id ⊗₁ (F.₁ B ∘ τ ∘ B)) ∘ B) ∘ α ≈⟨ {! !} ⟩ -- B swap - (F.₁ B ∘ τ ∘ B) ∘ (σ ⊗₁ id) ∘ α ≈⟨ {! !} ⟩ - (F.₁ (braiding.⇐.η (X ⊗₀ Y , Z)) ∘ t.η (Z , X ⊗₀ Y) ∘ braiding.⇒.η (F.₀ (X ⊗₀ Y) , Z)) ∘ (η' (X , Y) ⊗₁ id) ∘ associator.to ∎ - where - α = associator.to - α⁻¹ = associator.from - B : ∀ {X Y} → X ⊗₀ Y ⇒ Y ⊗₀ X - B {X} {Y} = braiding.⇒.η (X , Y) - τ : ∀ {X Y} → X ⊗₀ F.₀ Y ⇒ F.₀ (X ⊗₀ Y) - τ {X} {Y} = t.η (X , Y) - σ : ∀ {X Y} → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) - σ {X} {Y} = η' (X , Y) - -- strength.strength-assoc : F.₁ α⁻¹ ∘ τ ≈ τ ∘ (id × τ) ∘ α⁻¹ - braiding-eq : ∀ {X Y} → braiding.⇐.η (X , Y) ≈ braiding.⇒.η (Y , X) - braiding-eq = introʳ commutative ○ cancelˡ (braiding.iso.isoˡ _) + F.₁ α ∘ F.₁ (B (Y ⊗₀ Z , X)) ∘ t.η (Y ⊗₀ Z , X) ∘ B (F.₀ X , Y ⊗₀ Z) ≈⟨ {! !} ⟩ + (F.₁ (B (Z , X ⊗₀ Y)) ∘ t.η (Z , X ⊗₀ Y) ∘ B (F.₀ (X ⊗₀ Y) , Z)) ∘ (τ (X , Y) ⊗₁ id) ∘ associator.to ∎ + + StrongMonad⇒RightStrongMonad : StrongMonad V → RightStrongMonad V + StrongMonad⇒RightStrongMonad SM = record { M = M ; rightStrength = Strength⇒RightStrength strength } + where + open StrongMonad SM + + RightStrength⇒Strength : ∀ {M : Monad C} → RightStrength V M → Strength V M + RightStrength⇒Strength {M} rightStrength = {! !} + + RightStrongMonad⇒StrongMonad : RightStrongMonad V → StrongMonad V + RightStrongMonad⇒StrongMonad RSM = record { M = M ; strength = RightStrength⇒Strength rightStrength } + where + open RightStrongMonad RSM \ No newline at end of file From 6e4a64015205df317558aec4ca7194e0423f1c9a Mon Sep 17 00:00:00 2001 From: Sandro Stucki Date: Sat, 6 Jan 2024 19:10:01 +0100 Subject: [PATCH 06/15] [ wip ] proved that the induced right strength commutes with the associator. --- src/Categories/Monad/Strong/Properties.agda | 206 +++++++++++++++----- 1 file changed, 162 insertions(+), 44 deletions(-) diff --git a/src/Categories/Monad/Strong/Properties.agda b/src/Categories/Monad/Strong/Properties.agda index 427d5796d..fe935161b 100644 --- a/src/Categories/Monad/Strong/Properties.agda +++ b/src/Categories/Monad/Strong/Properties.agda @@ -7,12 +7,16 @@ module Categories.Monad.Strong.Properties where open import Level open import Data.Product using (_,_; _×_) -open import Categories.Category.Core +open import Categories.Category using (Category; module Commutation) +import Categories.Category.Construction.Core as Core open import Categories.Category.Product open import Categories.Functor renaming (id to idF) open import Categories.Category.Monoidal using (Monoidal) +import Categories.Category.Monoidal.Braided.Properties as BraidedProps +import Categories.Category.Monoidal.Reasoning as MonoidalReasoning +import Categories.Category.Monoidal.Utilities as MonoidalUtils open import Categories.Category.Monoidal.Symmetric using (Symmetric) -open import Categories.NaturalTransformation using (ntHelper) +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) open import Categories.Monad using (Monad) open import Categories.Monad.Strong using (Strength; RightStrength; StrongMonad; RightStrongMonad) @@ -22,73 +26,187 @@ private variable o ℓ e : Level +-- FIXME: make these top-level module parameters and remove this anonymous module? module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where open Category C open Symmetric S - open import Categories.Category.Monoidal.Braided.Properties braided - open HomReasoning - open Equiv + open BraidedProps braided using (braiding-coherence; inv-braiding-coherence) + open MonoidalUtils V using (_⊗ᵢ_) + open MonoidalUtils.Shorthands V -- for λ⇒, ρ⇒, α⇒, ... + open Core.Shorthands C -- for idᵢ, _∘ᵢ_, ... + open MonoidalReasoning V open MR C + open Commutation C + + private + variable + X Y Z W : Obj + + -- FIXME: this should probably go into + -- Categories.Monoidal.Symmetric.Properties and be called + -- braided-selfInverse or something similar. + braiding-eq : ∀ {X Y} → braiding.⇐.η (X , Y) ≈ braiding.⇒.η (Y , X) + braiding-eq = introʳ commutative ○ cancelˡ (braiding.iso.isoˡ _) + + module LeftStrength {M : Monad C} (leftStrength : Strength V M) where + open BraidedProps.Shorthands braided renaming (σ to B; σ⇒ to B⇒; σ⇐ to B⇐) + open Monad M using (F; μ; η) + module leftStrength = Strength leftStrength + + module Shorthands where + module σ = leftStrength.strengthen + + σ : ∀ {X Y} → X ⊗₀ F.₀ Y ⇒ F.₀ (X ⊗₀ Y) + σ {X} {Y} = σ.η (X , Y) + + open Shorthands + + -- The left strength induces a right strength + + private + τ : ∀ {X Y} → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) + τ {X} {Y} = F.₁ B⇒ ∘ σ ∘ B⇒ + + τ-commute : (f : X ⇒ Z) (g : Y ⇒ W) → τ ∘ (F.₁ f ⊗₁ g) ≈ F.₁ (f ⊗₁ g) ∘ τ + τ-commute f g = begin + (F.₁ B⇒ ∘ σ ∘ B⇒) ∘ (F.₁ f ⊗₁ g) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (F.₁ f , g))) ⟩ + F.₁ B⇒ ∘ σ ∘ ((g ⊗₁ F.₁ f) ∘ B⇒) ≈⟨ refl⟩∘⟨ pullˡ (σ.commute (g , f)) ⟩ + F.₁ B⇒ ∘ (F.₁ (g ⊗₁ f) ∘ σ) ∘ B⇒ ≈˘⟨ pushˡ (pushˡ (F.homomorphism)) ⟩ + (F.₁ (B⇒ ∘ (g ⊗₁ f)) ∘ σ) ∘ B⇒ ≈⟨ pushˡ (F.F-resp-≈ (braiding.⇒.commute (g , f)) ⟩∘⟨refl) ⟩ + F.₁ ((f ⊗₁ g) ∘ B⇒) ∘ σ ∘ B⇒ ≈⟨ pushˡ F.homomorphism ⟩ + F.₁ (f ⊗₁ g) ∘ F.₁ B⇒ ∘ σ ∘ B⇒ ∎ + + right-strengthen : NaturalTransformation (⊗ ∘F (F ⁂ idF)) (F ∘F ⊗) + right-strengthen = ntHelper (record + { η = λ _ → τ + ; commute = λ (f , g) → τ-commute f g + }) + + private module τ = NaturalTransformation right-strengthen + + -- The strengths commute with braiding + + left-right-braiding-comm : ∀ {X Y} → F.₁ B⇒ ∘ σ {X} {Y} ≈ τ ∘ B⇒ + left-right-braiding-comm = begin + F.₁ B⇒ ∘ σ ≈˘⟨ pullʳ (cancelʳ commutative) ⟩ + (F.₁ B⇒ ∘ σ ∘ B⇒) ∘ B⇒ ∎ + + right-left-braiding-comm : ∀ {X Y} → F.₁ B⇒ ∘ τ {X} {Y} ≈ σ ∘ B⇒ + right-left-braiding-comm = begin + F.₁ B⇒ ∘ (F.₁ B⇒ ∘ σ ∘ B⇒) ≈˘⟨ pushˡ F.homomorphism ⟩ + F.₁ (B⇒ ∘ B⇒) ∘ σ ∘ B⇒ ≈⟨ F.F-resp-≈ commutative ⟩∘⟨refl ⟩ + F.₁ id ∘ σ ∘ B⇒ ≈⟨ elimˡ F.identity ⟩ + σ ∘ B⇒ ∎ + + -- Reversing a ternary product via braiding commutes with the + -- associator. + -- + -- FIXME: this is a lemma just about associators and braiding, so + -- it should probably be exported to + -- Categories.Category.Monoidal.Braided.Properties. There might + -- also be a more straight-forward way to state and prove it. + + assoc-reverse : [ X ⊗₀ (Y ⊗₀ Z) ⇒ (X ⊗₀ Y) ⊗₀ Z ]⟨ + id ⊗₁ B⇒ ⇒⟨ X ⊗₀ (Z ⊗₀ Y) ⟩ + B⇒ ⇒⟨ (Z ⊗₀ Y) ⊗₀ X ⟩ + α⇒ ⇒⟨ Z ⊗₀ (Y ⊗₀ X) ⟩ + id ⊗₁ B⇐ ⇒⟨ Z ⊗₀ (X ⊗₀ Y) ⟩ + B⇐ + ≈ α⇐ + ⟩ + assoc-reverse = begin + B⇐ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ ≈˘⟨ refl⟩∘⟨ assoc²' ⟩ + B⇐ ∘ (id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒) ∘ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ pushˡ hex₁' ⟩ + B⇐ ∘ (α⇒ ∘ B⇒ ⊗₁ id) ∘ α⇐ ∘ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ pullʳ (sym-assoc ○ hexagon₂) ⟩ + B⇐ ∘ α⇒ ∘ (α⇐ ∘ B⇒) ∘ α⇐ ≈⟨ refl⟩∘⟨ pullˡ (cancelˡ associator.isoʳ) ⟩ + B⇐ ∘ B⇒ ∘ α⇐ ≈⟨ cancelˡ (braiding.iso.isoˡ _) ⟩ + α⇐ ∎ + where + hex₁' = conjugate-from associator (idᵢ ⊗ᵢ B) (⟺ (hexagon₁ ○ sym-assoc)) + + -- The induced right strength commutes with the associator + + right-strength-assoc : [ F.₀ X ⊗₀ (Y ⊗₀ Z) ⇒ F.₀ ((X ⊗₀ Y) ⊗₀ Z) ]⟨ + τ ⇒⟨ F.₀ (X ⊗₀ (Y ⊗₀ Z)) ⟩ + F.₁ α⇐ + ≈ α⇐ ⇒⟨ (F.₀ X ⊗₀ Y) ⊗₀ Z ⟩ + τ ⊗₁ id ⇒⟨ F.₀ (X ⊗₀ Y) ⊗₀ Z ⟩ + τ + ⟩ + right-strength-assoc = begin + F.₁ α⇐ ∘ τ + ≈˘⟨ F.F-resp-≈ assoc-reverse ⟩∘⟨refl ⟩ + F.₁ (B⇐ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒) ∘ τ + ≈⟨ pushˡ F.homomorphism ⟩ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒) ∘ τ + ≈⟨ F.F-resp-≈ braiding-eq ⟩∘⟨ pushˡ F.homomorphism ⟩ + F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ (α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒) ∘ τ + ≈⟨ refl⟩∘⟨ F.F-resp-≈ (refl⟩⊗⟨ braiding-eq) ⟩∘⟨ pushˡ F.homomorphism ⟩ + F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ F.₁ α⇒ ∘ F.₁ (B⇒ ∘ id ⊗₁ B⇒) ∘ τ + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ + F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ F.₁ α⇒ ∘ F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ τ + ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ τ.commute (id , B⇒) ⟩ + F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ F.₁ α⇒ ∘ F.₁ B⇒ ∘ τ ∘ F.₁ id ⊗₁ B⇒ + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ right-left-braiding-comm ⟩ + F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ F.₁ α⇒ ∘ σ ∘ B⇒ ∘ F.₁ id ⊗₁ B⇒ + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ leftStrength.strength-assoc ⟩ + F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ σ ∘ (id ⊗₁ σ ∘ α⇒) ∘ B⇒ ∘ F.₁ id ⊗₁ B⇒ + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ (refl⟩∘⟨ refl⟩∘⟨ F.identity ⟩⊗⟨refl) ⟩ + F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ σ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + ≈˘⟨ refl⟩∘⟨ extendʳ (σ.commute (id , B⇒)) ⟩ + F.₁ B⇒ ∘ σ ∘ id ⊗₁ F.₁ B⇒ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + ≈⟨ extendʳ left-right-braiding-comm ⟩ + τ ∘ B⇒ ∘ id ⊗₁ F.₁ B⇒ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (parallel Equiv.refl left-right-braiding-comm) ⟩ + τ ∘ B⇒ ∘ id ⊗₁ τ ∘ id ⊗₁ B⇒ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + ≈⟨ refl⟩∘⟨ extendʳ (braiding.⇒.commute (id , τ)) ⟩ + τ ∘ τ ⊗₁ id ∘ B⇒ ∘ id ⊗₁ B⇒ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟺ braiding-eq ⟩∘⟨ (refl⟩⊗⟨ ⟺ braiding-eq) ⟩∘⟨refl ⟩ + τ ∘ τ ⊗₁ id ∘ B⇐ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc-reverse ⟩ + τ ∘ τ ⊗₁ id ∘ α⇐ + ∎ Strength⇒RightStrength : ∀ {M : Monad C} → Strength V M → RightStrength V M Strength⇒RightStrength {M} strength = record - { strengthen = ntHelper (record - { η = τ - ; commute = λ (f , g) → commute' f g - }) + { strengthen = right-strengthen ; identityˡ = identityˡ' ; η-comm = η-comm' ; μ-η-comm = μ-η-comm' - ; strength-assoc = strength-assoc' + ; strength-assoc = right-strength-assoc } where + open LeftStrength strength open Monad M using (F; μ; η) module strength = Strength strength module t = strength.strengthen B = braiding.⇒.η τ : ∀ ((X , Y) : Obj × Obj) → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) τ (X , Y) = F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ B (F.₀ X , Y) - α = associator.to - α⁻¹ = associator.from - braiding-eq : ∀ {X Y} → braiding.⇐.η (X , Y) ≈ B (Y , X) - braiding-eq = introʳ commutative ○ cancelˡ (braiding.iso.isoˡ _) - commute' : ∀ {X Y U V : Obj} (f : X ⇒ U) (g : Y ⇒ V) → τ (U , V) ∘ (F.₁ f ⊗₁ g) ≈ F.₁ (f ⊗₁ g) ∘ τ (X , Y) - commute' {X} {Y} {U} {V} f g = begin - (F.₁ (B (V , U)) ∘ t.η (V , U) ∘ B (F.₀ U , V)) ∘ (F.₁ f ⊗₁ g) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (F.₁ f , g))) ⟩ - F.₁ (B (V , U)) ∘ t.η (V , U) ∘ ((g ⊗₁ F.₁ f) ∘ B (F.₀ X , Y)) ≈⟨ refl⟩∘⟨ pullˡ (t.commute (g , f)) ⟩ - F.₁ (B (V , U)) ∘ ((F.₁ (g ⊗₁ f) ∘ t.η (Y , X)) ∘ B (F.₀ X , Y)) ≈⟨ pullˡ (pullˡ (sym F.homomorphism)) ⟩ - (F.₁ (B (V , U) ∘ (g ⊗₁ f)) ∘ t.η (Y , X)) ∘ B (F.₀ X , Y) ≈⟨ F.F-resp-≈ (braiding.⇒.commute (g , f)) ⟩∘⟨refl ⟩∘⟨refl ⟩ - (F.₁ ((f ⊗₁ g) ∘ B (Y , X)) ∘ t.η (Y , X)) ∘ B (F.₀ X , Y) ≈⟨ pushˡ F.homomorphism ⟩∘⟨refl ⟩ - (F.₁ (f ⊗₁ g) ∘ F.₁ (B (Y , X)) ∘ t.η (Y , X)) ∘ B (F.₀ X , Y) ≈⟨ assoc²' ⟩ - (F.₁ (f ⊗₁ g) ∘ τ (X , Y)) ∎ identityˡ' : ∀ {X : Obj} → F.₁ unitorʳ.from ∘ τ (X , unit) ≈ unitorʳ.from - identityˡ' {X} = begin - F.₁ unitorʳ.from ∘ F.₁ (B (unit , X)) ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ pullˡ (sym F.homomorphism) ⟩ - F.₁ (unitorʳ.from ∘ B (unit , X)) ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ ((F.F-resp-≈ ((refl⟩∘⟨ sym braiding-eq) ○ inv-braiding-coherence)) ⟩∘⟨refl) ⟩ - F.₁ unitorˡ.from ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ pullˡ strength.identityˡ ⟩ - unitorˡ.from ∘ B (F.₀ X , unit) ≈⟨ braiding-coherence ⟩ + identityˡ' {X} = begin + F.₁ unitorʳ.from ∘ F.₁ (B (unit , X)) ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ pullˡ (⟺ F.homomorphism) ⟩ + F.₁ (unitorʳ.from ∘ B (unit , X)) ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ ((F.F-resp-≈ ((refl⟩∘⟨ ⟺ braiding-eq) ○ inv-braiding-coherence)) ⟩∘⟨refl) ⟩ + F.₁ unitorˡ.from ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ pullˡ strength.identityˡ ⟩ + unitorˡ.from ∘ B (F.₀ X , unit) ≈⟨ braiding-coherence ⟩ unitorʳ.from ∎ η-comm' : ∀ {X Y : Obj} → τ (X , Y) ∘ η.η X ⊗₁ id ≈ η.η (X ⊗₀ Y) - η-comm' {X} {Y} = begin - (F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ B (F.₀ X , Y)) ∘ (η.η X ⊗₁ id) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (η.η X , id))) ⟩ - F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ ((id ⊗₁ η.η X) ∘ B (X , Y)) ≈⟨ (refl⟩∘⟨ (pullˡ strength.η-comm)) ⟩ - F.₁ (B (Y , X)) ∘ η.η (Y ⊗₀ X) ∘ B (X , Y) ≈⟨ pullˡ (sym (η.commute (B (Y , X)))) ⟩ + η-comm' {X} {Y} = begin + (F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ B (F.₀ X , Y)) ∘ (η.η X ⊗₁ id) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (η.η X , id))) ⟩ + F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ ((id ⊗₁ η.η X) ∘ B (X , Y)) ≈⟨ (refl⟩∘⟨ (pullˡ strength.η-comm)) ⟩ + F.₁ (B (Y , X)) ∘ η.η (Y ⊗₀ X) ∘ B (X , Y) ≈⟨ pullˡ (⟺ (η.commute (B (Y , X)))) ⟩ (η.η (X ⊗₀ Y) ∘ B (Y , X)) ∘ B (X , Y) ≈⟨ cancelʳ commutative ⟩ η.η (X ⊗₀ Y) ∎ μ-η-comm' : ∀ {X Y : Obj} → μ.η (X ⊗₀ Y) ∘ F.₁ (τ (X , Y)) ∘ τ (F.₀ X , Y) ≈ τ (X , Y) ∘ μ.η X ⊗₁ id - μ-η-comm' {X} {Y} = begin - μ.η (X ⊗₀ Y) ∘ F.F₁ (τ (X , Y)) ∘ F.₁ (B (Y , F.₀ X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ (pullˡ (sym F.homomorphism))) ⟩ + μ-η-comm' {X} {Y} = begin + μ.η (X ⊗₀ Y) ∘ F.F₁ (τ (X , Y)) ∘ F.₁ (B (Y , F.₀ X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ (pullˡ (⟺ F.homomorphism))) ⟩ μ.η (X ⊗₀ Y) ∘ F.₁ (τ (X , Y) ∘ B (Y , F.₀ X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ ((F.F-resp-≈ (pullʳ (cancelʳ commutative))) ⟩∘⟨refl)) ⟩ - μ.η (X ⊗₀ Y) ∘ F.₁ (F.₁ (B (Y , X)) ∘ t.η (Y , X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ (F.homomorphism ⟩∘⟨refl)) ⟩ - μ.η (X ⊗₀ Y) ∘ (F.₁ (F.₁ (B (Y , X))) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ pullˡ (pullˡ (μ.commute (B (Y , X)))) ⟩ - ((F.₁ (B (Y , X)) ∘ μ.η (Y ⊗₀ X)) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (assoc² ○ (refl⟩∘⟨ sym assoc²')) ⟩ - F.₁ (B (Y , X)) ∘ (μ.η (Y ⊗₀ X) ∘ F.₁ (t.η (Y , X)) ∘ t.η (Y , F.₀ X)) ∘ B ((F.₀ (F.₀ X)) , Y) ≈⟨ refl⟩∘⟨ pushˡ strength.μ-η-comm ⟩ - F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ (id ⊗₁ μ.η X) ∘ B ((F.₀ (F.₀ X)) , Y) ≈˘⟨ pullʳ (pullʳ (braiding.⇒.commute (μ.η X , id))) ⟩ + μ.η (X ⊗₀ Y) ∘ F.₁ (F.₁ (B (Y , X)) ∘ t.η (Y , X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ (F.homomorphism ⟩∘⟨refl)) ⟩ + μ.η (X ⊗₀ Y) ∘ (F.₁ (F.₁ (B (Y , X))) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ pullˡ (pullˡ (μ.commute (B (Y , X)))) ⟩ + ((F.₁ (B (Y , X)) ∘ μ.η (Y ⊗₀ X)) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (assoc² ○ (refl⟩∘⟨ ⟺ assoc²')) ⟩ + F.₁ (B (Y , X)) ∘ (μ.η (Y ⊗₀ X) ∘ F.₁ (t.η (Y , X)) ∘ t.η (Y , F.₀ X)) ∘ B ((F.₀ (F.₀ X)) , Y) ≈⟨ refl⟩∘⟨ pushˡ strength.μ-η-comm ⟩ + F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ (id ⊗₁ μ.η X) ∘ B ((F.₀ (F.₀ X)) , Y) ≈˘⟨ pullʳ (pullʳ (braiding.⇒.commute (μ.η X , id))) ⟩ τ (X , Y) ∘ μ.η X ⊗₁ id ∎ - strength-assoc' : {X Y Z : Obj} → F.₁ associator.to ∘ τ (X , Y ⊗₀ Z) ≈ τ (X ⊗₀ Y , Z) ∘ τ (X , Y) ⊗₁ id ∘ associator.to - strength-assoc' {X} {Y} {Z} = begin - F.₁ α ∘ F.₁ (B (Y ⊗₀ Z , X)) ∘ t.η (Y ⊗₀ Z , X) ∘ B (F.₀ X , Y ⊗₀ Z) ≈⟨ {! !} ⟩ - (F.₁ (B (Z , X ⊗₀ Y)) ∘ t.η (Z , X ⊗₀ Y) ∘ B (F.₀ (X ⊗₀ Y) , Z)) ∘ (τ (X , Y) ⊗₁ id) ∘ associator.to ∎ StrongMonad⇒RightStrongMonad : StrongMonad V → RightStrongMonad V StrongMonad⇒RightStrongMonad SM = record { M = M ; rightStrength = Strength⇒RightStrength strength } @@ -102,4 +220,4 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where RightStrongMonad⇒StrongMonad RSM = record { M = M ; strength = RightStrength⇒Strength rightStrength } where open RightStrongMonad RSM - \ No newline at end of file + From 3bc122cbf6ca05155e1f7479d8edf21d024b4b42 Mon Sep 17 00:00:00 2001 From: Sandro Stucki Date: Sat, 6 Jan 2024 22:49:11 +0100 Subject: [PATCH 07/15] [ wip ] everything still works for braided categories (as opposed to symmetric). --- src/Categories/Monad/Strong/Properties.agda | 105 ++++++++++---------- 1 file changed, 50 insertions(+), 55 deletions(-) diff --git a/src/Categories/Monad/Strong/Properties.agda b/src/Categories/Monad/Strong/Properties.agda index fe935161b..901093410 100644 --- a/src/Categories/Monad/Strong/Properties.agda +++ b/src/Categories/Monad/Strong/Properties.agda @@ -1,6 +1,6 @@ {-# OPTIONS --without-K --safe #-} --- In symmetric monoidal categories left and right strength imply each other +-- In braided monoidal categories left and right strength imply each other module Categories.Monad.Strong.Properties where @@ -15,7 +15,7 @@ open import Categories.Category.Monoidal using (Monoidal) import Categories.Category.Monoidal.Braided.Properties as BraidedProps import Categories.Category.Monoidal.Reasoning as MonoidalReasoning import Categories.Category.Monoidal.Utilities as MonoidalUtils -open import Categories.Category.Monoidal.Symmetric using (Symmetric) +open import Categories.Category.Monoidal.Braided using (Braided) open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) open import Categories.Monad using (Monad) open import Categories.Monad.Strong using (Strength; RightStrength; StrongMonad; RightStrongMonad) @@ -27,10 +27,10 @@ private o ℓ e : Level -- FIXME: make these top-level module parameters and remove this anonymous module? -module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where +module _ {C : Category o ℓ e} {V : Monoidal C} (BV : Braided V) where open Category C - open Symmetric S - open BraidedProps braided using (braiding-coherence; inv-braiding-coherence) + open Braided BV + open BraidedProps BV using (braiding-coherence; inv-braiding-coherence) open MonoidalUtils V using (_⊗ᵢ_) open MonoidalUtils.Shorthands V -- for λ⇒, ρ⇒, α⇒, ... open Core.Shorthands C -- for idᵢ, _∘ᵢ_, ... @@ -42,14 +42,8 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where variable X Y Z W : Obj - -- FIXME: this should probably go into - -- Categories.Monoidal.Symmetric.Properties and be called - -- braided-selfInverse or something similar. - braiding-eq : ∀ {X Y} → braiding.⇐.η (X , Y) ≈ braiding.⇒.η (Y , X) - braiding-eq = introʳ commutative ○ cancelˡ (braiding.iso.isoˡ _) - module LeftStrength {M : Monad C} (leftStrength : Strength V M) where - open BraidedProps.Shorthands braided renaming (σ to B; σ⇒ to B⇒; σ⇐ to B⇐) + open BraidedProps.Shorthands BV renaming (σ to B; σ⇒ to B⇒; σ⇐ to B⇐) open Monad M using (F; μ; η) module leftStrength = Strength leftStrength @@ -61,20 +55,20 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where open Shorthands - -- The left strength induces a right strength + -- The left strength induces a right strength via braiding. private τ : ∀ {X Y} → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) - τ {X} {Y} = F.₁ B⇒ ∘ σ ∘ B⇒ + τ {X} {Y} = F.₁ B⇐ ∘ σ ∘ B⇒ τ-commute : (f : X ⇒ Z) (g : Y ⇒ W) → τ ∘ (F.₁ f ⊗₁ g) ≈ F.₁ (f ⊗₁ g) ∘ τ τ-commute f g = begin - (F.₁ B⇒ ∘ σ ∘ B⇒) ∘ (F.₁ f ⊗₁ g) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (F.₁ f , g))) ⟩ - F.₁ B⇒ ∘ σ ∘ ((g ⊗₁ F.₁ f) ∘ B⇒) ≈⟨ refl⟩∘⟨ pullˡ (σ.commute (g , f)) ⟩ - F.₁ B⇒ ∘ (F.₁ (g ⊗₁ f) ∘ σ) ∘ B⇒ ≈˘⟨ pushˡ (pushˡ (F.homomorphism)) ⟩ - (F.₁ (B⇒ ∘ (g ⊗₁ f)) ∘ σ) ∘ B⇒ ≈⟨ pushˡ (F.F-resp-≈ (braiding.⇒.commute (g , f)) ⟩∘⟨refl) ⟩ - F.₁ ((f ⊗₁ g) ∘ B⇒) ∘ σ ∘ B⇒ ≈⟨ pushˡ F.homomorphism ⟩ - F.₁ (f ⊗₁ g) ∘ F.₁ B⇒ ∘ σ ∘ B⇒ ∎ + (F.₁ B⇐ ∘ σ ∘ B⇒) ∘ (F.₁ f ⊗₁ g) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (F.₁ f , g))) ⟩ + F.₁ B⇐ ∘ σ ∘ ((g ⊗₁ F.₁ f) ∘ B⇒) ≈⟨ refl⟩∘⟨ pullˡ (σ.commute (g , f)) ⟩ + F.₁ B⇐ ∘ (F.₁ (g ⊗₁ f) ∘ σ) ∘ B⇒ ≈˘⟨ pushˡ (pushˡ (F.homomorphism)) ⟩ + (F.₁ (B⇐ ∘ (g ⊗₁ f)) ∘ σ) ∘ B⇒ ≈⟨ pushˡ (F.F-resp-≈ (braiding.⇐.commute (f , g)) ⟩∘⟨refl) ⟩ + F.₁ ((f ⊗₁ g) ∘ B⇐) ∘ σ ∘ B⇒ ≈⟨ pushˡ F.homomorphism ⟩ + F.₁ (f ⊗₁ g) ∘ F.₁ B⇐ ∘ σ ∘ B⇒ ∎ right-strengthen : NaturalTransformation (⊗ ∘F (F ⁂ idF)) (F ∘F ⊗) right-strengthen = ntHelper (record @@ -86,15 +80,15 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where -- The strengths commute with braiding - left-right-braiding-comm : ∀ {X Y} → F.₁ B⇒ ∘ σ {X} {Y} ≈ τ ∘ B⇒ + left-right-braiding-comm : ∀ {X Y} → F.₁ B⇐ ∘ σ {X} {Y} ≈ τ ∘ B⇐ left-right-braiding-comm = begin - F.₁ B⇒ ∘ σ ≈˘⟨ pullʳ (cancelʳ commutative) ⟩ - (F.₁ B⇒ ∘ σ ∘ B⇒) ∘ B⇒ ∎ + F.₁ B⇐ ∘ σ ≈˘⟨ pullʳ (cancelʳ (braiding.iso.isoʳ _)) ⟩ + (F.₁ B⇐ ∘ σ ∘ B⇒) ∘ B⇐ ∎ right-left-braiding-comm : ∀ {X Y} → F.₁ B⇒ ∘ τ {X} {Y} ≈ σ ∘ B⇒ right-left-braiding-comm = begin - F.₁ B⇒ ∘ (F.₁ B⇒ ∘ σ ∘ B⇒) ≈˘⟨ pushˡ F.homomorphism ⟩ - F.₁ (B⇒ ∘ B⇒) ∘ σ ∘ B⇒ ≈⟨ F.F-resp-≈ commutative ⟩∘⟨refl ⟩ + F.₁ B⇒ ∘ (F.₁ B⇐ ∘ σ ∘ B⇒) ≈˘⟨ pushˡ F.homomorphism ⟩ + F.₁ (B⇒ ∘ B⇐) ∘ σ ∘ B⇒ ≈⟨ F.F-resp-≈ (braiding.iso.isoʳ _) ⟩∘⟨refl ⟩ F.₁ id ∘ σ ∘ B⇒ ≈⟨ elimˡ F.identity ⟩ σ ∘ B⇒ ∎ @@ -139,29 +133,29 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where F.₁ (B⇐ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒) ∘ τ ≈⟨ pushˡ F.homomorphism ⟩ F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒) ∘ τ - ≈⟨ F.F-resp-≈ braiding-eq ⟩∘⟨ pushˡ F.homomorphism ⟩ - F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ (α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒) ∘ τ - ≈⟨ refl⟩∘⟨ F.F-resp-≈ (refl⟩⊗⟨ braiding-eq) ⟩∘⟨ pushˡ F.homomorphism ⟩ - F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ F.₁ α⇒ ∘ F.₁ (B⇒ ∘ id ⊗₁ B⇒) ∘ τ + ≈⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ (α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒) ∘ τ + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ α⇒ ∘ F.₁ (B⇒ ∘ id ⊗₁ B⇒) ∘ τ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ F.homomorphism ⟩ - F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ F.₁ α⇒ ∘ F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ τ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ α⇒ ∘ F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ τ ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ τ.commute (id , B⇒) ⟩ - F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ F.₁ α⇒ ∘ F.₁ B⇒ ∘ τ ∘ F.₁ id ⊗₁ B⇒ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ α⇒ ∘ F.₁ B⇒ ∘ τ ∘ F.₁ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ right-left-braiding-comm ⟩ - F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ F.₁ α⇒ ∘ σ ∘ B⇒ ∘ F.₁ id ⊗₁ B⇒ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ α⇒ ∘ σ ∘ B⇒ ∘ F.₁ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ leftStrength.strength-assoc ⟩ - F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ σ ∘ (id ⊗₁ σ ∘ α⇒) ∘ B⇒ ∘ F.₁ id ⊗₁ B⇒ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ σ ∘ (id ⊗₁ σ ∘ α⇒) ∘ B⇒ ∘ F.₁ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ (refl⟩∘⟨ refl⟩∘⟨ F.identity ⟩⊗⟨refl) ⟩ - F.₁ B⇒ ∘ F.₁ (id ⊗₁ B⇒) ∘ σ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ - ≈˘⟨ refl⟩∘⟨ extendʳ (σ.commute (id , B⇒)) ⟩ - F.₁ B⇒ ∘ σ ∘ id ⊗₁ F.₁ B⇒ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ σ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + ≈˘⟨ refl⟩∘⟨ extendʳ (σ.commute (id , B⇐)) ⟩ + F.₁ B⇐ ∘ σ ∘ id ⊗₁ F.₁ B⇐ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ ≈⟨ extendʳ left-right-braiding-comm ⟩ - τ ∘ B⇒ ∘ id ⊗₁ F.₁ B⇒ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + τ ∘ B⇐ ∘ id ⊗₁ F.₁ B⇐ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ (parallel Equiv.refl left-right-braiding-comm) ⟩ - τ ∘ B⇒ ∘ id ⊗₁ τ ∘ id ⊗₁ B⇒ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ - ≈⟨ refl⟩∘⟨ extendʳ (braiding.⇒.commute (id , τ)) ⟩ - τ ∘ τ ⊗₁ id ∘ B⇒ ∘ id ⊗₁ B⇒ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟺ braiding-eq ⟩∘⟨ (refl⟩⊗⟨ ⟺ braiding-eq) ⟩∘⟨refl ⟩ + τ ∘ B⇐ ∘ id ⊗₁ τ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + ≈⟨ refl⟩∘⟨ extendʳ (braiding.⇐.commute (τ , id)) ⟩ + τ ∘ τ ⊗₁ id ∘ B⇐ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ Equiv.refl ⟩∘⟨ (refl⟩⊗⟨ Equiv.refl) ⟩∘⟨refl ⟩ τ ∘ τ ⊗₁ id ∘ B⇐ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc-reverse ⟩ τ ∘ τ ⊗₁ id ∘ α⇐ @@ -181,31 +175,32 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where module strength = Strength strength module t = strength.strengthen B = braiding.⇒.η + open BraidedProps.Shorthands BV using () renaming (σ⇐ to B⇐) τ : ∀ ((X , Y) : Obj × Obj) → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) - τ (X , Y) = F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ B (F.₀ X , Y) + τ (X , Y) = F.₁ B⇐ ∘ t.η (Y , X) ∘ B (F.₀ X , Y) identityˡ' : ∀ {X : Obj} → F.₁ unitorʳ.from ∘ τ (X , unit) ≈ unitorʳ.from identityˡ' {X} = begin - F.₁ unitorʳ.from ∘ F.₁ (B (unit , X)) ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ pullˡ (⟺ F.homomorphism) ⟩ - F.₁ (unitorʳ.from ∘ B (unit , X)) ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ ((F.F-resp-≈ ((refl⟩∘⟨ ⟺ braiding-eq) ○ inv-braiding-coherence)) ⟩∘⟨refl) ⟩ + F.₁ unitorʳ.from ∘ F.₁ B⇐ ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ pullˡ (⟺ F.homomorphism) ⟩ + F.₁ (unitorʳ.from ∘ B⇐) ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ ((F.F-resp-≈ (inv-braiding-coherence)) ⟩∘⟨refl) ⟩ F.₁ unitorˡ.from ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ pullˡ strength.identityˡ ⟩ unitorˡ.from ∘ B (F.₀ X , unit) ≈⟨ braiding-coherence ⟩ unitorʳ.from ∎ η-comm' : ∀ {X Y : Obj} → τ (X , Y) ∘ η.η X ⊗₁ id ≈ η.η (X ⊗₀ Y) η-comm' {X} {Y} = begin - (F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ B (F.₀ X , Y)) ∘ (η.η X ⊗₁ id) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (η.η X , id))) ⟩ - F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ ((id ⊗₁ η.η X) ∘ B (X , Y)) ≈⟨ (refl⟩∘⟨ (pullˡ strength.η-comm)) ⟩ - F.₁ (B (Y , X)) ∘ η.η (Y ⊗₀ X) ∘ B (X , Y) ≈⟨ pullˡ (⟺ (η.commute (B (Y , X)))) ⟩ - (η.η (X ⊗₀ Y) ∘ B (Y , X)) ∘ B (X , Y) ≈⟨ cancelʳ commutative ⟩ + (F.₁ B⇐ ∘ t.η (Y , X) ∘ B (F.₀ X , Y)) ∘ (η.η X ⊗₁ id) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (η.η X , id))) ⟩ + F.₁ B⇐ ∘ t.η (Y , X) ∘ ((id ⊗₁ η.η X) ∘ B (X , Y)) ≈⟨ (refl⟩∘⟨ (pullˡ strength.η-comm)) ⟩ + F.₁ B⇐ ∘ η.η (Y ⊗₀ X) ∘ B (X , Y) ≈⟨ pullˡ (⟺ (η.commute B⇐)) ⟩ + (η.η (X ⊗₀ Y) ∘ B⇐) ∘ B (X , Y) ≈⟨ cancelʳ (braiding.iso.isoˡ _) ⟩ η.η (X ⊗₀ Y) ∎ μ-η-comm' : ∀ {X Y : Obj} → μ.η (X ⊗₀ Y) ∘ F.₁ (τ (X , Y)) ∘ τ (F.₀ X , Y) ≈ τ (X , Y) ∘ μ.η X ⊗₁ id μ-η-comm' {X} {Y} = begin - μ.η (X ⊗₀ Y) ∘ F.F₁ (τ (X , Y)) ∘ F.₁ (B (Y , F.₀ X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ (pullˡ (⟺ F.homomorphism))) ⟩ - μ.η (X ⊗₀ Y) ∘ F.₁ (τ (X , Y) ∘ B (Y , F.₀ X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ ((F.F-resp-≈ (pullʳ (cancelʳ commutative))) ⟩∘⟨refl)) ⟩ - μ.η (X ⊗₀ Y) ∘ F.₁ (F.₁ (B (Y , X)) ∘ t.η (Y , X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ (F.homomorphism ⟩∘⟨refl)) ⟩ - μ.η (X ⊗₀ Y) ∘ (F.₁ (F.₁ (B (Y , X))) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ pullˡ (pullˡ (μ.commute (B (Y , X)))) ⟩ - ((F.₁ (B (Y , X)) ∘ μ.η (Y ⊗₀ X)) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (assoc² ○ (refl⟩∘⟨ ⟺ assoc²')) ⟩ - F.₁ (B (Y , X)) ∘ (μ.η (Y ⊗₀ X) ∘ F.₁ (t.η (Y , X)) ∘ t.η (Y , F.₀ X)) ∘ B ((F.₀ (F.₀ X)) , Y) ≈⟨ refl⟩∘⟨ pushˡ strength.μ-η-comm ⟩ - F.₁ (B (Y , X)) ∘ t.η (Y , X) ∘ (id ⊗₁ μ.η X) ∘ B ((F.₀ (F.₀ X)) , Y) ≈˘⟨ pullʳ (pullʳ (braiding.⇒.commute (μ.η X , id))) ⟩ + μ.η (X ⊗₀ Y) ∘ F.₁ (τ (X , Y)) ∘ F.₁ B⇐ ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ refl⟩∘⟨ pullˡ (⟺ F.homomorphism) ⟩ + μ.η (X ⊗₀ Y) ∘ F.₁ (τ (X , Y) ∘ B⇐) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ ((F.F-resp-≈ (pullʳ (cancelʳ (braiding.iso.isoʳ _)))) ⟩∘⟨refl)) ⟩ + μ.η (X ⊗₀ Y) ∘ F.₁ (F.₁ B⇐ ∘ t.η (Y , X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ (F.homomorphism ⟩∘⟨refl)) ⟩ + μ.η (X ⊗₀ Y) ∘ (F.₁ (F.₁ B⇐) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ pullˡ (pullˡ (μ.commute B⇐)) ⟩ + ((F.₁ B⇐ ∘ μ.η (Y ⊗₀ X)) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (assoc² ○ (refl⟩∘⟨ ⟺ assoc²')) ⟩ + F.₁ B⇐ ∘ (μ.η (Y ⊗₀ X) ∘ F.₁ (t.η (Y , X)) ∘ t.η (Y , F.₀ X)) ∘ B ((F.₀ (F.₀ X)) , Y) ≈⟨ refl⟩∘⟨ pushˡ strength.μ-η-comm ⟩ + F.₁ B⇐ ∘ t.η (Y , X) ∘ (id ⊗₁ μ.η X) ∘ B ((F.₀ (F.₀ X)) , Y) ≈˘⟨ pullʳ (pullʳ (braiding.⇒.commute (μ.η X , id))) ⟩ τ (X , Y) ∘ μ.η X ⊗₁ id ∎ StrongMonad⇒RightStrongMonad : StrongMonad V → RightStrongMonad V From e82a53b0d176c4c89f2a39ff985745c0b657a7c1 Mon Sep 17 00:00:00 2001 From: Sandro Stucki Date: Sun, 7 Jan 2024 00:28:00 +0100 Subject: [PATCH 08/15] Add reverse of monoidal categories. --- .../Monoidal/Construction/Reverse.agda | 137 ++++++++++++++++++ 1 file changed, 137 insertions(+) create mode 100644 src/Categories/Category/Monoidal/Construction/Reverse.agda diff --git a/src/Categories/Category/Monoidal/Construction/Reverse.agda b/src/Categories/Category/Monoidal/Construction/Reverse.agda new file mode 100644 index 000000000..6dc270186 --- /dev/null +++ b/src/Categories/Category/Monoidal/Construction/Reverse.agda @@ -0,0 +1,137 @@ +{-# OPTIONS --without-K --safe #-} + +module Categories.Category.Monoidal.Construction.Reverse where + +-- The reverse monoidal category of a monoidal category V has the same +-- underlying category and unit as V but reversed monoidal product, +-- and similarly for tensors of morphisms. +-- +-- https://ncatlab.org/nlab/show/reverse+monoidal+category + +open import Level using (_⊔_) +open import Data.Product using (_,_; swap) +import Function + +open import Categories.Category using (Category) +open import Categories.Category.Monoidal +open import Categories.Category.Monoidal.Braided using (Braided) +import Categories.Category.Monoidal.Braided.Properties as BraidedProperties +open import Categories.Category.Monoidal.Symmetric using (Symmetric) +import Categories.Category.Monoidal.Utilities as MonoidalUtils +import Categories.Morphism as Morphism +import Categories.Morphism.Reasoning as MorphismReasoning +open import Categories.Functor.Bifunctor using (Bifunctor) +open import Categories.NaturalTransformation.NaturalIsomorphism using (niHelper) + +open Category using (Obj) + +module _ {o ℓ e} {C : Category o ℓ e} (M : Monoidal C) where + + private module M = Monoidal M + + open Function using (_∘_) + open Category C using (sym-assoc) + open Category.HomReasoning C using (⟺; _○_) + open Morphism C using (module ≅) + open MorphismReasoning C using (switch-fromtoʳ) + open MonoidalUtils M using (pentagon-inv) + + ⊗ : Bifunctor C C C + ⊗ = record + { F₀ = M.⊗.₀ ∘ swap + ; F₁ = M.⊗.₁ ∘ swap + ; identity = M.⊗.identity + ; homomorphism = M.⊗.homomorphism + ; F-resp-≈ = M.⊗.F-resp-≈ ∘ swap + } + + Reverse-Monoidal : Monoidal C + Reverse-Monoidal = record + { ⊗ = ⊗ + ; unit = M.unit + ; unitorˡ = M.unitorʳ + ; unitorʳ = M.unitorˡ + ; associator = ≅.sym M.associator + ; unitorˡ-commute-from = M.unitorʳ-commute-from + ; unitorˡ-commute-to = M.unitorʳ-commute-to + ; unitorʳ-commute-from = M.unitorˡ-commute-from + ; unitorʳ-commute-to = M.unitorˡ-commute-to + ; assoc-commute-from = M.assoc-commute-to + ; assoc-commute-to = M.assoc-commute-from + ; triangle = ⟺ (switch-fromtoʳ M.associator M.triangle) + ; pentagon = sym-assoc ○ pentagon-inv + } + +module _ {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} where + + open Category C using (assoc; sym-assoc) + open Category.HomReasoning C using (_○_) + + -- The reverse of a braided category is again braided. + + Reverse-Braided : Braided M → Braided (Reverse-Monoidal M) + Reverse-Braided BM = record + { braiding = niHelper (record + { η = braiding.⇐.η + ; η⁻¹ = braiding.⇒.η + ; commute = braiding.⇐.commute + ; iso = λ XY → record + { isoˡ = braiding.iso.isoʳ XY + ; isoʳ = braiding.iso.isoˡ XY } + }) + ; hexagon₁ = sym-assoc ○ hexagon₁-inv ○ assoc + ; hexagon₂ = assoc ○ hexagon₂-inv ○ sym-assoc + } + where + open Braided BM + open BraidedProperties BM using (hexagon₁-inv; hexagon₂-inv) + + -- The reverse of a symmetric category is again symmetric. + + Reverse-Symmetric : Symmetric M → Symmetric (Reverse-Monoidal M) + Reverse-Symmetric SM = record + { braided = Reverse-Braided braided + ; commutative = commutative′ + } + where + open Symmetric SM + + -- FIXME: the below should probably go into + -- Categories.Monoidal.Symmetric.Properties, but we currently + -- have no such module. + + open Category C + open MorphismReasoning C using (introʳ; cancelˡ) + + braiding-selfInverse : ∀ {X Y} → braiding.⇐.η (X , Y) ≈ braiding.⇒.η (Y , X) + braiding-selfInverse = introʳ commutative ○ cancelˡ (braiding.iso.isoˡ _) + + commutative′ : ∀ {X Y} → braiding.⇐.η (X , Y) ∘ braiding.⇐.η (Y , X) ≈ id + commutative′ = ∘-resp-≈ braiding-selfInverse braiding-selfInverse ○ commutative + +-- Bundled versions of the above + +Reverse-MonoidalCategory : ∀ {o ℓ e} → MonoidalCategory o ℓ e → MonoidalCategory o ℓ e +Reverse-MonoidalCategory C = record + { U = U + ; monoidal = Reverse-Monoidal monoidal + } + where open MonoidalCategory C + +Reverse-BraidedMonoidalCategory : ∀ {o ℓ e} → + BraidedMonoidalCategory o ℓ e → BraidedMonoidalCategory o ℓ e +Reverse-BraidedMonoidalCategory C = record + { U = U + ; monoidal = Reverse-Monoidal monoidal + ; braided = Reverse-Braided braided + } + where open BraidedMonoidalCategory C + +Reverse-SymmetricMonoidalCategory : ∀ {o ℓ e} → + SymmetricMonoidalCategory o ℓ e → SymmetricMonoidalCategory o ℓ e +Reverse-SymmetricMonoidalCategory C = record + { U = U + ; monoidal = Reverse-Monoidal monoidal + ; symmetric = Reverse-Symmetric symmetric + } + where open SymmetricMonoidalCategory C From a1edce063e576b6e5b36df623f147bbc118edaa5 Mon Sep 17 00:00:00 2001 From: Sandro Stucki Date: Sun, 7 Jan 2024 00:32:07 +0100 Subject: [PATCH 09/15] [ wip ] finish proof that a right strength induces a left strength in a braided category. --- src/Categories/Monad/Strong/Properties.agda | 162 ++++++++++++++------ 1 file changed, 118 insertions(+), 44 deletions(-) diff --git a/src/Categories/Monad/Strong/Properties.agda b/src/Categories/Monad/Strong/Properties.agda index 901093410..2aac54a8e 100644 --- a/src/Categories/Monad/Strong/Properties.agda +++ b/src/Categories/Monad/Strong/Properties.agda @@ -1,61 +1,89 @@ {-# OPTIONS --without-K --safe #-} --- In braided monoidal categories left and right strength imply each other +open import Categories.Category using (Category; module Commutation) -module Categories.Monad.Strong.Properties where +module Categories.Monad.Strong.Properties {o ℓ e} {C : Category o ℓ e} where open import Level open import Data.Product using (_,_; _×_) -open import Categories.Category using (Category; module Commutation) import Categories.Category.Construction.Core as Core open import Categories.Category.Product open import Categories.Functor renaming (id to idF) open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Braided using (Braided) +open import Categories.Category.Monoidal.Construction.Reverse + using (Reverse-Monoidal; Reverse-Braided) import Categories.Category.Monoidal.Braided.Properties as BraidedProps import Categories.Category.Monoidal.Reasoning as MonoidalReasoning import Categories.Category.Monoidal.Utilities as MonoidalUtils -open import Categories.Category.Monoidal.Braided using (Braided) -open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) open import Categories.Monad using (Monad) open import Categories.Monad.Strong using (Strength; RightStrength; StrongMonad; RightStrongMonad) - import Categories.Morphism.Reasoning as MR +open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper) -private - variable - o ℓ e : Level +-- A left strength is a right strength in the reversed category. --- FIXME: make these top-level module parameters and remove this anonymous module? -module _ {C : Category o ℓ e} {V : Monoidal C} (BV : Braided V) where +rightInReversed : {V : Monoidal C} {M : Monad C} → + Strength V M → RightStrength (Reverse-Monoidal V) M +rightInReversed left = record + { strengthen = ntHelper (record + { η = λ{ (X , Y) → strengthen.η (Y , X) } + ; commute = λ{ (f , g) → strengthen.commute (g , f) } + }) + ; identityˡ = identityˡ + ; η-comm = η-comm + ; μ-η-comm = μ-η-comm + ; strength-assoc = strength-assoc + } + where open Strength left + +-- A right strength is a left strength in the reversed category. + +leftInReversed : {V : Monoidal C} {M : Monad C} → + RightStrength V M → Strength (Reverse-Monoidal V) M +leftInReversed right = record + { strengthen = ntHelper (record + { η = λ{ (X , Y) → strengthen.η (Y , X) } + ; commute = λ{ (f , g) → strengthen.commute (g , f) } + }) + ; identityˡ = identityˡ + ; η-comm = η-comm + ; μ-η-comm = μ-η-comm + ; strength-assoc = strength-assoc + } + where open RightStrength right + + +module Left {V : Monoidal C} {M : Monad C} (left : Strength V M) where open Category C - open Braided BV - open BraidedProps BV using (braiding-coherence; inv-braiding-coherence) - open MonoidalUtils V using (_⊗ᵢ_) - open MonoidalUtils.Shorthands V -- for λ⇒, ρ⇒, α⇒, ... - open Core.Shorthands C -- for idᵢ, _∘ᵢ_, ... - open MonoidalReasoning V + open Core.Shorthands C -- for idᵢ, _∘ᵢ_, ... open MR C open Commutation C + open Monoidal V using (_⊗₀_) + open MonoidalUtils V using (_⊗ᵢ_) + open MonoidalUtils.Shorthands V -- for λ⇒, ρ⇒, α⇒, ... + open MonoidalReasoning V + open Monad M using (F; μ; η) private + module left = Strength left variable X Y Z W : Obj - module LeftStrength {M : Monad C} (leftStrength : Strength V M) where - open BraidedProps.Shorthands BV renaming (σ to B; σ⇒ to B⇒; σ⇐ to B⇐) - open Monad M using (F; μ; η) - module leftStrength = Strength leftStrength + module Shorthands where + module σ = left.strengthen - module Shorthands where - module σ = leftStrength.strengthen + σ : ∀ {X Y} → X ⊗₀ F.₀ Y ⇒ F.₀ (X ⊗₀ Y) + σ {X} {Y} = σ.η (X , Y) - σ : ∀ {X Y} → X ⊗₀ F.₀ Y ⇒ F.₀ (X ⊗₀ Y) - σ {X} {Y} = σ.η (X , Y) + open Shorthands - open Shorthands + -- In a braided monoidal category, a left strength induces a right strength. - -- The left strength induces a right strength via braiding. + module _ (BV : Braided V) where + open Braided BV hiding (_⊗₀_) + open BraidedProps.Shorthands BV renaming (σ to B; σ⇒ to B⇒; σ⇐ to B⇐) private τ : ∀ {X Y} → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) @@ -143,7 +171,7 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (BV : Braided V) where F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ α⇒ ∘ F.₁ B⇒ ∘ τ ∘ F.₁ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ right-left-braiding-comm ⟩ F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ F.₁ α⇒ ∘ σ ∘ B⇒ ∘ F.₁ id ⊗₁ B⇒ - ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ leftStrength.strength-assoc ⟩ + ≈⟨ refl⟩∘⟨ refl⟩∘⟨ extendʳ left.strength-assoc ⟩ F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ σ ∘ (id ⊗₁ σ ∘ α⇒) ∘ B⇒ ∘ F.₁ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ pullʳ (refl⟩∘⟨ refl⟩∘⟨ F.identity ⟩⊗⟨refl) ⟩ F.₁ B⇐ ∘ F.₁ (id ⊗₁ B⇐) ∘ σ ∘ id ⊗₁ σ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ @@ -161,18 +189,18 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (BV : Braided V) where τ ∘ τ ⊗₁ id ∘ α⇐ ∎ - Strength⇒RightStrength : ∀ {M : Monad C} → Strength V M → RightStrength V M - Strength⇒RightStrength {M} strength = record - { strengthen = right-strengthen + Strength⇒RightStrength : (BV : Braided V) → RightStrength V M + Strength⇒RightStrength BV = record + { strengthen = right-strengthen BV ; identityˡ = identityˡ' ; η-comm = η-comm' ; μ-η-comm = μ-η-comm' - ; strength-assoc = right-strength-assoc + ; strength-assoc = right-strength-assoc BV } where - open LeftStrength strength - open Monad M using (F; μ; η) - module strength = Strength strength + open Braided BV hiding (_⊗₀_) + open BraidedProps BV using (braiding-coherence; inv-braiding-coherence) + module strength = Strength left module t = strength.strengthen B = braiding.⇒.η open BraidedProps.Shorthands BV using () renaming (σ⇐ to B⇐) @@ -203,16 +231,62 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (BV : Braided V) where F.₁ B⇐ ∘ t.η (Y , X) ∘ (id ⊗₁ μ.η X) ∘ B ((F.₀ (F.₀ X)) , Y) ≈˘⟨ pullʳ (pullʳ (braiding.⇒.commute (μ.η X , id))) ⟩ τ (X , Y) ∘ μ.η X ⊗₁ id ∎ - StrongMonad⇒RightStrongMonad : StrongMonad V → RightStrongMonad V - StrongMonad⇒RightStrongMonad SM = record { M = M ; rightStrength = Strength⇒RightStrength strength } - where - open StrongMonad SM +StrongMonad⇒RightStrongMonad : {V : Monoidal C} → + Braided V → StrongMonad V → RightStrongMonad V +StrongMonad⇒RightStrongMonad BV SM = record + { M = M + ; rightStrength = Left.Strength⇒RightStrength strength BV + } + where open StrongMonad SM + +module Right {V : Monoidal C} {M : Monad C} (right : RightStrength V M) where + + open Category C using (_⇒_) + open Monoidal V using (_⊗₀_) + open Monad M using (F) + + private module right = RightStrength right - RightStrength⇒Strength : ∀ {M : Monad C} → RightStrength V M → Strength V M - RightStrength⇒Strength {M} rightStrength = {! !} + module Shorthands where + module τ = right.strengthen - RightStrongMonad⇒StrongMonad : RightStrongMonad V → StrongMonad V - RightStrongMonad⇒StrongMonad RSM = record { M = M ; strength = RightStrength⇒Strength rightStrength } + τ : ∀ {X Y} → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) + τ {X} {Y} = τ.η (X , Y) + + open Shorthands + + -- In a braided monoidal category, a right strength induces a left strength. + + RightStrength⇒Strength : Braided V → Strength V M + RightStrength⇒Strength BV = record + { strengthen = strengthen + ; identityˡ = identityˡ + ; η-comm = η-comm + ; μ-η-comm = μ-η-comm + ; strength-assoc = strength-assoc + } where - open RightStrongMonad RSM + left₁ : Strength (Reverse-Monoidal V) M + left₁ = leftInReversed right + + right₂ : RightStrength (Reverse-Monoidal V) M + right₂ = Left.Strength⇒RightStrength left₁ (Reverse-Braided BV) + + -- Note: this is almost what we need, but Reverse-Monoidal is + -- not a strict involution (some of the coherence laws are + -- have proofs that are not strictly identical to their + -- original counterparts). But this does not matter + -- structurally, so we can just re-package the components we + -- need. + left₂ : Strength (Reverse-Monoidal (Reverse-Monoidal V)) M + left₂ = leftInReversed right₂ + + open Strength left₂ +RightStrongMonad⇒StrongMonad : {V : Monoidal C} → + Braided V → RightStrongMonad V → StrongMonad V +RightStrongMonad⇒StrongMonad BV RSM = record + { M = M + ; strength = Right.RightStrength⇒Strength rightStrength BV + } + where open RightStrongMonad RSM From adc716d63dd5607b3411aa6397f29df1fa2cb781 Mon Sep 17 00:00:00 2001 From: Sandro Stucki Date: Sun, 7 Jan 2024 01:26:52 +0100 Subject: [PATCH 10/15] [ wip ] make Categories.Monad.Commutative type check again and some cleanup. --- src/Categories/Monad/Commutative.agda | 8 +- src/Categories/Monad/Strong/Properties.agda | 155 ++++++++++---------- 2 files changed, 82 insertions(+), 81 deletions(-) diff --git a/src/Categories/Monad/Commutative.agda b/src/Categories/Monad/Commutative.agda index c7fb3b4f8..a25f8d111 100644 --- a/src/Categories/Monad/Commutative.agda +++ b/src/Categories/Monad/Commutative.agda @@ -24,9 +24,9 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where open Category C open Symmetric S open StrongMonad LSM - + rightStrength : RightStrength V M - rightStrength = Strength⇒RightStrength S strength + rightStrength = Strength⇒RightStrength braided strength private module LS = Strength strength @@ -43,7 +43,7 @@ module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where field strongMonad : StrongMonad V commutative : Commutative strongMonad - + open StrongMonad strongMonad public open Commutative commutative public - \ No newline at end of file + diff --git a/src/Categories/Monad/Strong/Properties.agda b/src/Categories/Monad/Strong/Properties.agda index 2aac54a8e..37d837e73 100644 --- a/src/Categories/Monad/Strong/Properties.agda +++ b/src/Categories/Monad/Strong/Properties.agda @@ -54,14 +54,15 @@ leftInReversed right = record } where open RightStrength right +open Category C hiding (identityˡ) +open MR C +open Commutation C module Left {V : Monoidal C} {M : Monad C} (left : Strength V M) where - open Category C - open Core.Shorthands C -- for idᵢ, _∘ᵢ_, ... - open MR C - open Commutation C + open Category C using (identityˡ) open Monoidal V using (_⊗₀_) open MonoidalUtils V using (_⊗ᵢ_) + open Core.Shorthands C -- for idᵢ, _∘ᵢ_, ... open MonoidalUtils.Shorthands V -- for λ⇒, ρ⇒, α⇒, ... open MonoidalReasoning V open Monad M using (F; μ; η) @@ -83,6 +84,7 @@ module Left {V : Monoidal C} {M : Monad C} (left : Strength V M) where module _ (BV : Braided V) where open Braided BV hiding (_⊗₀_) + open BraidedProps BV using (braiding-coherence; inv-braiding-coherence) open BraidedProps.Shorthands BV renaming (σ to B; σ⇒ to B⇒; σ⇐ to B⇐) private @@ -106,7 +108,7 @@ module Left {V : Monoidal C} {M : Monad C} (left : Strength V M) where private module τ = NaturalTransformation right-strengthen - -- The strengths commute with braiding + -- The strengths commute with braiding. left-right-braiding-comm : ∀ {X Y} → F.₁ B⇐ ∘ σ {X} {Y} ≈ τ ∘ B⇐ left-right-braiding-comm = begin @@ -120,6 +122,37 @@ module Left {V : Monoidal C} {M : Monad C} (left : Strength V M) where F.₁ id ∘ σ ∘ B⇒ ≈⟨ elimˡ F.identity ⟩ σ ∘ B⇒ ∎ + right-identityˡ : ∀ {X} → F.₁ ρ⇒ ∘ τ {X} {unit} ≈ ρ⇒ + right-identityˡ = begin + F.₁ ρ⇒ ∘ F.₁ B⇐ ∘ σ ∘ B⇒ ≈⟨ pullˡ (⟺ F.homomorphism) ⟩ + F.₁ (ρ⇒ ∘ B⇐) ∘ σ ∘ B⇒ ≈⟨ F.F-resp-≈ (inv-braiding-coherence) ⟩∘⟨refl ⟩ + F.₁ λ⇒ ∘ σ ∘ B⇒ ≈⟨ pullˡ left.identityˡ ⟩ + λ⇒ ∘ B⇒ ≈⟨ braiding-coherence ⟩ + ρ⇒ ∎ + + -- The induced right strength commutes with the monad unit. + + right-η-comm : ∀ {X Y} → τ ∘ η.η X ⊗₁ id ≈ η.η (X ⊗₀ Y) + right-η-comm {X} {Y} = begin + (F.₁ B⇐ ∘ σ ∘ B⇒) ∘ (η.η X ⊗₁ id) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (η.η X , id))) ⟩ + F.₁ B⇐ ∘ σ ∘ (id ⊗₁ η.η X) ∘ B⇒ ≈⟨ refl⟩∘⟨ pullˡ left.η-comm ⟩ + F.₁ B⇐ ∘ η.η (Y ⊗₀ X) ∘ B⇒ ≈⟨ pullˡ (⟺ (η.commute B⇐)) ⟩ + (η.η (X ⊗₀ Y) ∘ B⇐) ∘ B⇒ ≈⟨ cancelʳ (braiding.iso.isoˡ _) ⟩ + η.η (X ⊗₀ Y) ∎ + + -- The induced right strength commutes with the monad multiplication. + + right-μ-η-comm : ∀ {X Y} → μ.η (X ⊗₀ Y) ∘ F.₁ τ ∘ τ ≈ τ ∘ μ.η X ⊗₁ id + right-μ-η-comm {X} {Y} = begin + μ.η (X ⊗₀ Y) ∘ F.₁ τ ∘ F.₁ B⇐ ∘ σ ∘ B⇒ ≈⟨ refl⟩∘⟨ pullˡ (⟺ F.homomorphism) ⟩ + μ.η (X ⊗₀ Y) ∘ F.₁ (τ ∘ B⇐) ∘ σ ∘ B⇒ ≈⟨ refl⟩∘⟨ (F.F-resp-≈ (pullʳ (cancelʳ (braiding.iso.isoʳ _))) ⟩∘⟨refl) ⟩ + μ.η (X ⊗₀ Y) ∘ F.₁ (F.₁ B⇐ ∘ σ) ∘ σ ∘ B⇒ ≈⟨ refl⟩∘⟨ F.homomorphism ⟩∘⟨refl ⟩ + μ.η (X ⊗₀ Y) ∘ (F.₁ (F.₁ B⇐) ∘ F.₁ σ) ∘ σ ∘ B⇒ ≈⟨ pullˡ (pullˡ (μ.commute B⇐)) ⟩ + ((F.₁ B⇐ ∘ μ.η (Y ⊗₀ X)) ∘ F.₁ σ) ∘ σ ∘ B⇒ ≈⟨ assoc² ○ (refl⟩∘⟨ ⟺ assoc²') ⟩ + F.₁ B⇐ ∘ (μ.η (Y ⊗₀ X) ∘ F.₁ σ ∘ σ) ∘ B⇒ ≈⟨ refl⟩∘⟨ pushˡ left.μ-η-comm ⟩ + F.₁ B⇐ ∘ σ ∘ (id ⊗₁ μ.η X) ∘ B⇒ ≈˘⟨ pullʳ (pullʳ (braiding.⇒.commute (μ.η X , id))) ⟩ + τ ∘ μ.η X ⊗₁ id ∎ + -- Reversing a ternary product via braiding commutes with the -- associator. -- @@ -189,59 +222,26 @@ module Left {V : Monoidal C} {M : Monad C} (left : Strength V M) where τ ∘ τ ⊗₁ id ∘ α⇐ ∎ - Strength⇒RightStrength : (BV : Braided V) → RightStrength V M - Strength⇒RightStrength BV = record - { strengthen = right-strengthen BV - ; identityˡ = identityˡ' - ; η-comm = η-comm' - ; μ-η-comm = μ-η-comm' - ; strength-assoc = right-strength-assoc BV - } - where - open Braided BV hiding (_⊗₀_) - open BraidedProps BV using (braiding-coherence; inv-braiding-coherence) - module strength = Strength left - module t = strength.strengthen - B = braiding.⇒.η - open BraidedProps.Shorthands BV using () renaming (σ⇐ to B⇐) - τ : ∀ ((X , Y) : Obj × Obj) → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) - τ (X , Y) = F.₁ B⇐ ∘ t.η (Y , X) ∘ B (F.₀ X , Y) - identityˡ' : ∀ {X : Obj} → F.₁ unitorʳ.from ∘ τ (X , unit) ≈ unitorʳ.from - identityˡ' {X} = begin - F.₁ unitorʳ.from ∘ F.₁ B⇐ ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ pullˡ (⟺ F.homomorphism) ⟩ - F.₁ (unitorʳ.from ∘ B⇐) ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ ((F.F-resp-≈ (inv-braiding-coherence)) ⟩∘⟨refl) ⟩ - F.₁ unitorˡ.from ∘ t.η (unit , X) ∘ B (F.₀ X , unit) ≈⟨ pullˡ strength.identityˡ ⟩ - unitorˡ.from ∘ B (F.₀ X , unit) ≈⟨ braiding-coherence ⟩ - unitorʳ.from ∎ - η-comm' : ∀ {X Y : Obj} → τ (X , Y) ∘ η.η X ⊗₁ id ≈ η.η (X ⊗₀ Y) - η-comm' {X} {Y} = begin - (F.₁ B⇐ ∘ t.η (Y , X) ∘ B (F.₀ X , Y)) ∘ (η.η X ⊗₁ id) ≈⟨ pullʳ (pullʳ (braiding.⇒.commute (η.η X , id))) ⟩ - F.₁ B⇐ ∘ t.η (Y , X) ∘ ((id ⊗₁ η.η X) ∘ B (X , Y)) ≈⟨ (refl⟩∘⟨ (pullˡ strength.η-comm)) ⟩ - F.₁ B⇐ ∘ η.η (Y ⊗₀ X) ∘ B (X , Y) ≈⟨ pullˡ (⟺ (η.commute B⇐)) ⟩ - (η.η (X ⊗₀ Y) ∘ B⇐) ∘ B (X , Y) ≈⟨ cancelʳ (braiding.iso.isoˡ _) ⟩ - η.η (X ⊗₀ Y) ∎ - μ-η-comm' : ∀ {X Y : Obj} → μ.η (X ⊗₀ Y) ∘ F.₁ (τ (X , Y)) ∘ τ (F.₀ X , Y) ≈ τ (X , Y) ∘ μ.η X ⊗₁ id - μ-η-comm' {X} {Y} = begin - μ.η (X ⊗₀ Y) ∘ F.₁ (τ (X , Y)) ∘ F.₁ B⇐ ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ refl⟩∘⟨ pullˡ (⟺ F.homomorphism) ⟩ - μ.η (X ⊗₀ Y) ∘ F.₁ (τ (X , Y) ∘ B⇐) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ ((F.F-resp-≈ (pullʳ (cancelʳ (braiding.iso.isoʳ _)))) ⟩∘⟨refl)) ⟩ - μ.η (X ⊗₀ Y) ∘ F.₁ (F.₁ B⇐ ∘ t.η (Y , X)) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (refl⟩∘⟨ (F.homomorphism ⟩∘⟨refl)) ⟩ - μ.η (X ⊗₀ Y) ∘ (F.₁ (F.₁ B⇐) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ pullˡ (pullˡ (μ.commute B⇐)) ⟩ - ((F.₁ B⇐ ∘ μ.η (Y ⊗₀ X)) ∘ F.₁ (t.η (Y , X))) ∘ t.η (Y , F.₀ X) ∘ B (F.₀ (F.₀ X) , Y) ≈⟨ (assoc² ○ (refl⟩∘⟨ ⟺ assoc²')) ⟩ - F.₁ B⇐ ∘ (μ.η (Y ⊗₀ X) ∘ F.₁ (t.η (Y , X)) ∘ t.η (Y , F.₀ X)) ∘ B ((F.₀ (F.₀ X)) , Y) ≈⟨ refl⟩∘⟨ pushˡ strength.μ-η-comm ⟩ - F.₁ B⇐ ∘ t.η (Y , X) ∘ (id ⊗₁ μ.η X) ∘ B ((F.₀ (F.₀ X)) , Y) ≈˘⟨ pullʳ (pullʳ (braiding.⇒.commute (μ.η X , id))) ⟩ - τ (X , Y) ∘ μ.η X ⊗₁ id ∎ +Strength⇒RightStrength : {V : Monoidal C} {M : Monad C} → + Braided V → Strength V M → RightStrength V M +Strength⇒RightStrength BV left = record + { strengthen = right-strengthen BV + ; identityˡ = right-identityˡ BV + ; η-comm = right-η-comm BV + ; μ-η-comm = right-μ-η-comm BV + ; strength-assoc = right-strength-assoc BV + } + where open Left left StrongMonad⇒RightStrongMonad : {V : Monoidal C} → Braided V → StrongMonad V → RightStrongMonad V StrongMonad⇒RightStrongMonad BV SM = record { M = M - ; rightStrength = Left.Strength⇒RightStrength strength BV + ; rightStrength = Strength⇒RightStrength BV strength } where open StrongMonad SM module Right {V : Monoidal C} {M : Monad C} (right : RightStrength V M) where - - open Category C using (_⇒_) open Monoidal V using (_⊗₀_) open Monad M using (F) @@ -255,38 +255,39 @@ module Right {V : Monoidal C} {M : Monad C} (right : RightStrength V M) where open Shorthands - -- In a braided monoidal category, a right strength induces a left strength. - - RightStrength⇒Strength : Braided V → Strength V M - RightStrength⇒Strength BV = record - { strengthen = strengthen - ; identityˡ = identityˡ - ; η-comm = η-comm - ; μ-η-comm = μ-η-comm - ; strength-assoc = strength-assoc - } - where - left₁ : Strength (Reverse-Monoidal V) M - left₁ = leftInReversed right - - right₂ : RightStrength (Reverse-Monoidal V) M - right₂ = Left.Strength⇒RightStrength left₁ (Reverse-Braided BV) - - -- Note: this is almost what we need, but Reverse-Monoidal is - -- not a strict involution (some of the coherence laws are - -- have proofs that are not strictly identical to their - -- original counterparts). But this does not matter - -- structurally, so we can just re-package the components we - -- need. - left₂ : Strength (Reverse-Monoidal (Reverse-Monoidal V)) M - left₂ = leftInReversed right₂ - - open Strength left₂ +-- In a braided monoidal category, a right strength induces a left strength. + +RightStrength⇒Strength : {V : Monoidal C} {M : Monad C} → + Braided V → RightStrength V M → Strength V M +RightStrength⇒Strength {V} {M} BV right = record + { strengthen = strengthen + ; identityˡ = identityˡ + ; η-comm = η-comm + ; μ-η-comm = μ-η-comm + ; strength-assoc = strength-assoc + } + where + left₁ : Strength (Reverse-Monoidal V) M + left₁ = leftInReversed right + + right₂ : RightStrength (Reverse-Monoidal V) M + right₂ = Strength⇒RightStrength (Reverse-Braided BV) left₁ + + -- Note: this is almost what we need, but Reverse-Monoidal is + -- not a strict involution (some of the coherence laws are + -- have proofs that are not strictly identical to their + -- original counterparts). But this does not matter + -- structurally, so we can just re-package the components we + -- need. + left₂ : Strength (Reverse-Monoidal (Reverse-Monoidal V)) M + left₂ = leftInReversed right₂ + + open Strength left₂ RightStrongMonad⇒StrongMonad : {V : Monoidal C} → Braided V → RightStrongMonad V → StrongMonad V RightStrongMonad⇒StrongMonad BV RSM = record { M = M - ; strength = Right.RightStrength⇒Strength rightStrength BV + ; strength = RightStrength⇒Strength BV rightStrength } where open RightStrongMonad RSM From 8d48ec0b75d3acc709ee187d87533f8e9d4709f8 Mon Sep 17 00:00:00 2001 From: Sandro Stucki Date: Sat, 13 Jan 2024 15:59:26 +0100 Subject: [PATCH 11/15] Add extra coherence property for braided monoidal categories. --- .../Category/Monoidal/Braided/Properties.agda | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/Categories/Category/Monoidal/Braided/Properties.agda b/src/Categories/Category/Monoidal/Braided/Properties.agda index a63e7fe31..c10b45946 100644 --- a/src/Categories/Category/Monoidal/Braided/Properties.agda +++ b/src/Categories/Category/Monoidal/Braided/Properties.agda @@ -156,3 +156,23 @@ inv-braiding-coherence : [ unit ⊗₀ X ⇒ X ]⟨ ≈ λ⇒ ⟩ inv-braiding-coherence = ⟺ (switch-fromtoʳ σ braiding-coherence) + +-- Reversing a ternary product via braiding commutes with the associator. + +assoc-reverse : [ X ⊗₀ (Y ⊗₀ Z) ⇒ (X ⊗₀ Y) ⊗₀ Z ]⟨ + id ⊗₁ σ⇒ ⇒⟨ X ⊗₀ (Z ⊗₀ Y) ⟩ + σ⇒ ⇒⟨ (Z ⊗₀ Y) ⊗₀ X ⟩ + α⇒ ⇒⟨ Z ⊗₀ (Y ⊗₀ X) ⟩ + id ⊗₁ σ⇐ ⇒⟨ Z ⊗₀ (X ⊗₀ Y) ⟩ + σ⇐ + ≈ α⇐ + ⟩ +assoc-reverse = begin + σ⇐ ∘ id ⊗₁ σ⇐ ∘ α⇒ ∘ σ⇒ ∘ id ⊗₁ σ⇒ ≈˘⟨ refl⟩∘⟨ assoc²' ⟩ + σ⇐ ∘ (id ⊗₁ σ⇐ ∘ α⇒ ∘ σ⇒) ∘ id ⊗₁ σ⇒ ≈⟨ refl⟩∘⟨ pushˡ hex₁' ⟩ + σ⇐ ∘ (α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐ ∘ id ⊗₁ σ⇒ ≈⟨ refl⟩∘⟨ pullʳ (sym-assoc ○ hexagon₂) ⟩ + σ⇐ ∘ α⇒ ∘ (α⇐ ∘ σ⇒) ∘ α⇐ ≈⟨ refl⟩∘⟨ pullˡ (cancelˡ associator.isoʳ) ⟩ + σ⇐ ∘ σ⇒ ∘ α⇐ ≈⟨ cancelˡ (braiding.iso.isoˡ _) ⟩ + α⇐ ∎ + where + hex₁' = conjugate-from associator (idᵢ ⊗ᵢ σ) (⟺ (hexagon₁ ○ sym-assoc)) From 187e9cf7465b730196c5194a066d67e89f6b2bec Mon Sep 17 00:00:00 2001 From: Sandro Stucki Date: Sat, 13 Jan 2024 16:01:32 +0100 Subject: [PATCH 12/15] Add module with properties and shorthands for symmetric monoidal categories. --- .../Monoidal/Symmetric/Properties.agda | 29 +++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 src/Categories/Category/Monoidal/Symmetric/Properties.agda diff --git a/src/Categories/Category/Monoidal/Symmetric/Properties.agda b/src/Categories/Category/Monoidal/Symmetric/Properties.agda new file mode 100644 index 000000000..5bd48e767 --- /dev/null +++ b/src/Categories/Category/Monoidal/Symmetric/Properties.agda @@ -0,0 +1,29 @@ +{-# OPTIONS --without-K --safe #-} + +open import Categories.Category using (Category) +open import Categories.Category.Monoidal using (Monoidal) +open import Categories.Category.Monoidal.Symmetric using (Symmetric) + +module Categories.Category.Monoidal.Symmetric.Properties + {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} (SM : Symmetric M) where + +open import Data.Product using (_,_) + +import Categories.Category.Monoidal.Braided.Properties as BraidedProperties +open import Categories.Morphism.Reasoning C + +open Category C +open HomReasoning +open Symmetric SM + +-- Shorthands for the braiding + +open BraidedProperties braided public using (module Shorthands) + +-- Extra properties of the braiding in a symmetric monoidal category + +braiding-selfInverse : ∀ {X Y} → braiding.⇐.η (X , Y) ≈ braiding.⇒.η (Y , X) +braiding-selfInverse = introʳ commutative ○ cancelˡ (braiding.iso.isoˡ _) + +inv-commutative : ∀ {X Y} → braiding.⇐.η (X , Y) ∘ braiding.⇐.η (Y , X) ≈ id +inv-commutative = ∘-resp-≈ braiding-selfInverse braiding-selfInverse ○ commutative From cc9ec7f09565e251b5f8953cebdc593e1ab2a88a Mon Sep 17 00:00:00 2001 From: Sandro Stucki Date: Sat, 13 Jan 2024 16:03:32 +0100 Subject: [PATCH 13/15] Clean up reverse monoidal categories. --- .../Monoidal/Construction/Reverse.agda | 19 ++++--------------- 1 file changed, 4 insertions(+), 15 deletions(-) diff --git a/src/Categories/Category/Monoidal/Construction/Reverse.agda b/src/Categories/Category/Monoidal/Construction/Reverse.agda index 6dc270186..a4f338071 100644 --- a/src/Categories/Category/Monoidal/Construction/Reverse.agda +++ b/src/Categories/Category/Monoidal/Construction/Reverse.agda @@ -16,6 +16,7 @@ open import Categories.Category using (Category) open import Categories.Category.Monoidal open import Categories.Category.Monoidal.Braided using (Braided) import Categories.Category.Monoidal.Braided.Properties as BraidedProperties +import Categories.Category.Monoidal.Symmetric.Properties as SymmetricProperties open import Categories.Category.Monoidal.Symmetric using (Symmetric) import Categories.Category.Monoidal.Utilities as MonoidalUtils import Categories.Morphism as Morphism @@ -91,23 +92,11 @@ module _ {o ℓ e} {C : Category o ℓ e} {M : Monoidal C} where Reverse-Symmetric : Symmetric M → Symmetric (Reverse-Monoidal M) Reverse-Symmetric SM = record { braided = Reverse-Braided braided - ; commutative = commutative′ + ; commutative = inv-commutative } where - open Symmetric SM - - -- FIXME: the below should probably go into - -- Categories.Monoidal.Symmetric.Properties, but we currently - -- have no such module. - - open Category C - open MorphismReasoning C using (introʳ; cancelˡ) - - braiding-selfInverse : ∀ {X Y} → braiding.⇐.η (X , Y) ≈ braiding.⇒.η (Y , X) - braiding-selfInverse = introʳ commutative ○ cancelˡ (braiding.iso.isoˡ _) - - commutative′ : ∀ {X Y} → braiding.⇐.η (X , Y) ∘ braiding.⇐.η (Y , X) ≈ id - commutative′ = ∘-resp-≈ braiding-selfInverse braiding-selfInverse ○ commutative + open Symmetric SM using (braided) + open SymmetricProperties SM using (inv-commutative) -- Bundled versions of the above From 8d6f58a50f39b5b0e39ec99dc352604f0122b3b3 Mon Sep 17 00:00:00 2001 From: Sandro Stucki Date: Sat, 13 Jan 2024 16:05:25 +0100 Subject: [PATCH 14/15] Clean up properties of strengths and strong monads. --- src/Categories/Monad/Strong/Properties.agda | 54 ++++++--------------- 1 file changed, 14 insertions(+), 40 deletions(-) diff --git a/src/Categories/Monad/Strong/Properties.agda b/src/Categories/Monad/Strong/Properties.agda index 37d837e73..9ce9de1b9 100644 --- a/src/Categories/Monad/Strong/Properties.agda +++ b/src/Categories/Monad/Strong/Properties.agda @@ -84,7 +84,7 @@ module Left {V : Monoidal C} {M : Monad C} (left : Strength V M) where module _ (BV : Braided V) where open Braided BV hiding (_⊗₀_) - open BraidedProps BV using (braiding-coherence; inv-braiding-coherence) + open BraidedProps BV using (braiding-coherence; inv-braiding-coherence; assoc-reverse) open BraidedProps.Shorthands BV renaming (σ to B; σ⇒ to B⇒; σ⇐ to B⇐) private @@ -153,32 +153,6 @@ module Left {V : Monoidal C} {M : Monad C} (left : Strength V M) where F.₁ B⇐ ∘ σ ∘ (id ⊗₁ μ.η X) ∘ B⇒ ≈˘⟨ pullʳ (pullʳ (braiding.⇒.commute (μ.η X , id))) ⟩ τ ∘ μ.η X ⊗₁ id ∎ - -- Reversing a ternary product via braiding commutes with the - -- associator. - -- - -- FIXME: this is a lemma just about associators and braiding, so - -- it should probably be exported to - -- Categories.Category.Monoidal.Braided.Properties. There might - -- also be a more straight-forward way to state and prove it. - - assoc-reverse : [ X ⊗₀ (Y ⊗₀ Z) ⇒ (X ⊗₀ Y) ⊗₀ Z ]⟨ - id ⊗₁ B⇒ ⇒⟨ X ⊗₀ (Z ⊗₀ Y) ⟩ - B⇒ ⇒⟨ (Z ⊗₀ Y) ⊗₀ X ⟩ - α⇒ ⇒⟨ Z ⊗₀ (Y ⊗₀ X) ⟩ - id ⊗₁ B⇐ ⇒⟨ Z ⊗₀ (X ⊗₀ Y) ⟩ - B⇐ - ≈ α⇐ - ⟩ - assoc-reverse = begin - B⇐ ∘ id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒ ∘ id ⊗₁ B⇒ ≈˘⟨ refl⟩∘⟨ assoc²' ⟩ - B⇐ ∘ (id ⊗₁ B⇐ ∘ α⇒ ∘ B⇒) ∘ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ pushˡ hex₁' ⟩ - B⇐ ∘ (α⇒ ∘ B⇒ ⊗₁ id) ∘ α⇐ ∘ id ⊗₁ B⇒ ≈⟨ refl⟩∘⟨ pullʳ (sym-assoc ○ hexagon₂) ⟩ - B⇐ ∘ α⇒ ∘ (α⇐ ∘ B⇒) ∘ α⇐ ≈⟨ refl⟩∘⟨ pullˡ (cancelˡ associator.isoʳ) ⟩ - B⇐ ∘ B⇒ ∘ α⇐ ≈⟨ cancelˡ (braiding.iso.isoˡ _) ⟩ - α⇐ ∎ - where - hex₁' = conjugate-from associator (idᵢ ⊗ᵢ B) (⟺ (hexagon₁ ○ sym-assoc)) - -- The induced right strength commutes with the associator right-strength-assoc : [ F.₀ X ⊗₀ (Y ⊗₀ Z) ⇒ F.₀ ((X ⊗₀ Y) ⊗₀ Z) ]⟨ @@ -222,16 +196,20 @@ module Left {V : Monoidal C} {M : Monad C} (left : Strength V M) where τ ∘ τ ⊗₁ id ∘ α⇐ ∎ + -- The induced right strength + + right : RightStrength V M + right = record + { strengthen = right-strengthen + ; identityˡ = right-identityˡ + ; η-comm = right-η-comm + ; μ-η-comm = right-μ-η-comm + ; strength-assoc = right-strength-assoc + } + Strength⇒RightStrength : {V : Monoidal C} {M : Monad C} → Braided V → Strength V M → RightStrength V M -Strength⇒RightStrength BV left = record - { strengthen = right-strengthen BV - ; identityˡ = right-identityˡ BV - ; η-comm = right-η-comm BV - ; μ-η-comm = right-μ-η-comm BV - ; strength-assoc = right-strength-assoc BV - } - where open Left left +Strength⇒RightStrength BV left = Left.right left BV StrongMonad⇒RightStrongMonad : {V : Monoidal C} → Braided V → StrongMonad V → RightStrongMonad V @@ -245,16 +223,12 @@ module Right {V : Monoidal C} {M : Monad C} (right : RightStrength V M) where open Monoidal V using (_⊗₀_) open Monad M using (F) - private module right = RightStrength right - module Shorthands where - module τ = right.strengthen + module τ = RightStrength.strengthen right τ : ∀ {X Y} → F.₀ X ⊗₀ Y ⇒ F.₀ (X ⊗₀ Y) τ {X} {Y} = τ.η (X , Y) - open Shorthands - -- In a braided monoidal category, a right strength induces a left strength. RightStrength⇒Strength : {V : Monoidal C} {M : Monad C} → From 40de5643f814ea7619c7e71b6f2535ead28f506b Mon Sep 17 00:00:00 2001 From: Sandro Stucki Date: Sat, 13 Jan 2024 16:06:29 +0100 Subject: [PATCH 15/15] Clean up commutative monads. --- src/Categories/Monad/Commutative.agda | 27 +++++++++++---------------- 1 file changed, 11 insertions(+), 16 deletions(-) diff --git a/src/Categories/Monad/Commutative.agda b/src/Categories/Monad/Commutative.agda index a25f8d111..2f75e000a 100644 --- a/src/Categories/Monad/Commutative.agda +++ b/src/Categories/Monad/Commutative.agda @@ -1,6 +1,6 @@ {-# OPTIONS --without-K --safe #-} --- Commutative Monad on a symmetric monoidal category +-- Commutative Monad on a braided monoidal category -- https://ncatlab.org/nlab/show/commutative+monad module Categories.Monad.Commutative where @@ -10,31 +10,26 @@ open import Data.Product using (_,_) open import Categories.Category.Core using (Category) open import Categories.Category.Monoidal using (Monoidal) -open import Categories.Category.Monoidal.Symmetric using (Symmetric) +open import Categories.Category.Monoidal.Braided using (Braided) open import Categories.Monad using (Monad) open import Categories.Monad.Strong using (StrongMonad; RightStrength; Strength) -open import Categories.Monad.Strong.Properties using (Strength⇒RightStrength) +import Categories.Monad.Strong.Properties as StrongProps private variable o ℓ e : Level -module _ {C : Category o ℓ e} {V : Monoidal C} (S : Symmetric V) where +module _ {C : Category o ℓ e} {V : Monoidal C} (B : Braided V) where record Commutative (LSM : StrongMonad V) : Set (o ⊔ ℓ ⊔ e) where - open Category C - open Symmetric S - open StrongMonad LSM + open Category C using (_⇒_; _∘_; _≈_) + open Braided B using (_⊗₀_) + open StrongMonad LSM using (M; strength) + open StrongProps.Left.Shorthands strength rightStrength : RightStrength V M - rightStrength = Strength⇒RightStrength braided strength - - private - module LS = Strength strength - module RS = RightStrength rightStrength - σ : ∀ {X Y} → X ⊗₀ M.F.₀ Y ⇒ M.F.₀ (X ⊗₀ Y) - σ {X} {Y} = LS.strengthen.η (X , Y) - τ : ∀ {X Y} → M.F.₀ X ⊗₀ Y ⇒ M.F.₀ (X ⊗₀ Y) - τ {X} {Y} = RS.strengthen.η (X , Y) + rightStrength = StrongProps.Strength⇒RightStrength B strength + + open StrongProps.Right.Shorthands rightStrength field commutes : ∀ {X Y} → M.μ.η (X ⊗₀ Y) ∘ M.F.₁ τ ∘ σ ≈ M.μ.η (X ⊗₀ Y) ∘ M.F.₁ σ ∘ τ