Extend monoidalize functor to commutative monoids

1 files changed, 100 insertions, 0 deletions

diff --git a/Functor/Monoidal/Construction/CMonoidValued.agda b/Functor/Monoidal/Construction/CMonoidValued.agda
new file mode 100644
index 0000000..2ac8be2
--- /dev/null
+++ b/Functor/Monoidal/Construction/CMonoidValued.agda
@@ -0,0 +1,100 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category using (Category)
+open import Categories.Category.Cocartesian using (Cocartesian)
+open import Category.Construction.CMonoids using (CMonoids)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Functor using (Functor) renaming (_∘F_ to _∙_)
+open import Level using (Level; _⊔_)
+
+-- A functor from a cocartesian category 𝒞 to CMonoids[S]
+-- can be turned into a symmetric monoidal functor from 𝒞 to S
+
+module Functor.Monoidal.Construction.CMonoidValued
+    {o o′ ℓ ℓ′ e e′ : Level}
+    {𝒞 : Category o ℓ e}
+    (𝒞-+ : Cocartesian 𝒞)
+    {S : SymmetricMonoidalCategory o′ ℓ′ e′}
+    (let module S = SymmetricMonoidalCategory S)
+    (M : Functor 𝒞 (CMonoids S.symmetric))
+  where
+
+import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
+import Categories.Morphism.Reasoning as ⇒-Reasoning
+import Object.Monoid.Commutative as CommutativeMonoidObject
+import Functor.Monoidal.Construction.MonoidValued as MonoidValued
+
+open import Categories.Category.Cocartesian using (module CocartesianSymmetricMonoidal)
+open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
+open import Categories.Category.Construction.Monoids using (Monoids)
+open import Categories.Category.Monoidal.Symmetric.Properties using (module Shorthands)
+open import Categories.Functor.Monoidal.Symmetric using (module Lax)
+open import Categories.Functor.Properties using ([_]-resp-∘)
+open import Data.Product using (_,_)
+open import Functor.Forgetful.Instance.CMonoid S.symmetric using (Forget)
+open import Functor.Forgetful.Instance.Monoid S.monoidal using () renaming (Forget to Forgetₘ)
+
+private
+
+  G : Functor 𝒞 (Monoids S.monoidal)
+  G = Forget ∙ M
+
+  H : Functor 𝒞 S.U
+  H = Forgetₘ ∙ G
+
+  module 𝒞 = CocartesianCategory (record { cocartesian = 𝒞-+ })
+  module 𝒞-SM = CocartesianSymmetricMonoidal 𝒞 𝒞-+
+
+  𝒞-SMC : SymmetricMonoidalCategory o ℓ e
+  𝒞-SMC = record { symmetric = 𝒞-SM.+-symmetric }
+
+  module H = Functor H
+  module M = Functor M
+
+  open CommutativeMonoidObject S.symmetric using (CommutativeMonoid; CommutativeMonoid⇒)
+  open CommutativeMonoid using (μ; Carrier) renaming (commutative to μ-commutative)
+  open CommutativeMonoid⇒
+  open 𝒞 using (_+_; i₁; i₂; inject₁; inject₂; +-swap)
+  open S
+  open ⇒-Reasoning U
+  open ⊗-Reasoning monoidal
+  open Shorthands symmetric
+
+  ⊲ : {A : 𝒞.Obj} → H.₀ A ⊗₀ H.₀ A ⇒ H.₀ A
+  ⊲ {A} = μ (M.₀ A)
+
+  ⇒⊲ : {A B : 𝒞.Obj} (f : A 𝒞.⇒ B) → H.₁ f ∘ ⊲ ≈ ⊲ ∘ H.₁ f ⊗₁ H.₁ f
+  ⇒⊲ f = preserves-μ (M.₁ f)
+
+  ⊲-⊗ : {n m : 𝒞.Obj} → H.₀ n ⊗₀ H.₀ m ⇒ H.₀ (n + m)
+  ⊲-⊗ = ⊲ ∘ H.₁ i₁ ⊗₁ H.₁ i₂
+
+  ⊲-σ : {n : 𝒞.Obj} → ⊲ {n} ≈ ⊲ ∘ σ⇒
+  ⊲-σ {A} = μ-commutative (M.₀ A)
+
+  braiding-compat
+      : {n m : 𝒞.Obj}
+      → H.₁ +-swap ∘ ⊲-⊗ {n} {m}
+      ≈ ⊲-⊗ ∘ σ⇒ {H.₀ n} {H.₀ m}
+  braiding-compat {n} {m} = begin
+      H.₁ +-swap ∘ ⊲-⊗ {n} {m}                                    ≡⟨⟩
+      H.₁ +-swap ∘ ⊲ {n + m} ∘ H.₁ i₁ ⊗₁ H.₁ i₂                   ≈⟨ extendʳ (⇒⊲ +-swap) ⟩
+      ⊲ {m + n} ∘ H.₁ +-swap ⊗₁ H.₁ +-swap ∘ H.₁ i₁ ⊗₁ H.₁ i₂     ≈⟨ refl⟩∘⟨ ⊗-distrib-over-∘ ⟨
+      ⊲ {m + n} ∘ (H.₁ +-swap ∘ H.₁ i₁) ⊗₁ (H.₁ +-swap ∘ H.₁ i₂)  ≈⟨ refl⟩∘⟨ [ H ]-resp-∘ inject₁ ⟩⊗⟨ [ H ]-resp-∘ inject₂ ⟩
+      ⊲ {m + n} ∘ H.₁ i₂ ⊗₁ H.₁ i₁                                ≈⟨ ⊲-σ ⟩∘⟨refl ⟩
+      (⊲ {m + n} ∘ σ⇒) ∘ H.₁ i₂ ⊗₁ H.₁ i₁                         ≈⟨ extendˡ (braiding.⇒.commute (H.₁ i₂ , H.₁ i₁)) ⟩
+      (⊲ {m + n} ∘ H.₁ i₁ ⊗₁ H.₁ i₂) ∘ σ⇒                         ≡⟨⟩
+      ⊲-⊗ {m} {n} ∘ σ⇒ {H.₀ n} {H.₀ m}                            ∎
+
+open MonoidValued 𝒞-+ G using (F,⊗,ε)
+
+F,⊗,ε,σ : Lax.SymmetricMonoidalFunctor 𝒞-SMC S
+F,⊗,ε,σ = record
+    { F,⊗,ε
+    ; isBraidedMonoidal = record
+        { F,⊗,ε
+        ; braiding-compat = braiding-compat
+        }
+    }
+
+module F,⊗,ε,σ = Lax.SymmetricMonoidalFunctor F,⊗,ε,σ