[WIP] Commutative Monad

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))

src/Categories/Category/Monoidal/Construction/Reverse.agda

@@ -0,0 +1,126 @@
+{-# 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
+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
+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 = inv-commutative
+    }
+    where
+      open Symmetric SM using (braided)
+      open SymmetricProperties SM using (inv-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

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

src/Categories/Monad/Commutative.agda

@@ -0,0 +1,44 @@
+{-# OPTIONS --without-K --safe #-}
+
+-- Commutative Monad on a braided 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 using (Category)
+open import Categories.Category.Monoidal using (Monoidal)
+open import Categories.Category.Monoidal.Braided using (Braided)
+open import Categories.Monad using (Monad)
+open import Categories.Monad.Strong using (StrongMonad; RightStrength; Strength)
+import Categories.Monad.Strong.Properties as StrongProps
+
+private
+  variable
+    o ℓ e : Level
+
+module _ {C : Category o ℓ e} {V : Monoidal C} (B : Braided V) where
+  record Commutative (LSM : StrongMonad V) : Set (o ⊔ ℓ ⊔ e) where
+    open Category C using (_⇒_; _∘_; _≈_)
+    open Braided B using (_⊗₀_)
+    open StrongMonad LSM using (M; strength)
+    open StrongProps.Left.Shorthands strength
+
+    rightStrength : RightStrength V M
+    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.₁ σ ∘ τ
+
+  record CommutativeMonad : Set (o ⊔ ℓ ⊔ e) where
+    field
+      strongMonad : StrongMonad V
+      commutative : Commutative strongMonad
+
+    open StrongMonad strongMonad public
+    open Commutative commutative public
+

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
@@ -42,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
@@ -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