Extend monoidalize functor to commutative monoids

4 files changed, 262 insertions, 0 deletions

diff --git a/Category/Construction/SymmetricMonoidalFunctors.agda b/Category/Construction/SymmetricMonoidalFunctors.agda
new file mode 100644
index 0000000..b5bf135
--- /dev/null
+++ b/Category/Construction/SymmetricMonoidalFunctors.agda
@@ -0,0 +1,59 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+
+module Category.Construction.SymmetricMonoidalFunctors
+    {o ℓ e o′ ℓ′ e′}
+    (C : SymmetricMonoidalCategory o ℓ e)
+    (D : SymmetricMonoidalCategory o′ ℓ′ e′)
+  where
+
+-- The functor category for a given pair of symmetric monoidal categories
+
+open import Level using (_⊔_)
+open import Relation.Binary.Construct.On using (isEquivalence)
+open import Categories.Category using (Category)
+open import Categories.Category.Helper using (categoryHelper)
+open import Categories.Functor.Monoidal.Symmetric using () renaming (module Lax to Lax₁; module Strong to Strong₁)
+open import Categories.NaturalTransformation.Monoidal.Symmetric using () renaming (module Lax to Lax₂; module Strong to Strong₂)
+open import Categories.NaturalTransformation.Equivalence using (_≃_; ≃-isEquivalence)
+
+open SymmetricMonoidalCategory D
+
+module Lax where
+
+  open Lax₂.SymmetricMonoidalNaturalTransformation using (U)
+
+  SymmetricMonoidalFunctors
+      : Category (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) (o ⊔ e′)
+  SymmetricMonoidalFunctors = categoryHelper record
+      { Obj = Lax₁.SymmetricMonoidalFunctor C D
+      ; _⇒_ = Lax₂.SymmetricMonoidalNaturalTransformation
+      ; _≈_ = λ α β → U α ≃ U β
+      ; id  = Lax₂.id
+      ; _∘_ = Lax₂._∘ᵥ_
+      ; assoc = assoc
+      ; identityˡ = identityˡ
+      ; identityʳ = identityʳ
+      ; equiv = isEquivalence U ≃-isEquivalence
+      ; ∘-resp-≈ = λ α₁≈β₁ α₂≈β₂ → ∘-resp-≈ α₁≈β₁ α₂≈β₂
+      }
+
+module Strong where
+
+  open Strong₂.SymmetricMonoidalNaturalTransformation using (U)
+
+  SymmetricMonoidalFunctors
+      : Category (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) (o ⊔ e′)
+  SymmetricMonoidalFunctors = categoryHelper record
+      { Obj = Strong₁.SymmetricMonoidalFunctor C D
+      ; _⇒_ = Strong₂.SymmetricMonoidalNaturalTransformation
+      ; _≈_ = λ α β → U α ≃ U β
+      ; id = Strong₂.id
+      ; _∘_ = Strong₂._∘ᵥ_
+      ; assoc = assoc
+      ; identityˡ = identityˡ
+      ; identityʳ = identityʳ
+      ; equiv = isEquivalence U ≃-isEquivalence
+      ; ∘-resp-≈ = λ α₁≈β₁ α₂≈β₂ → ∘-resp-≈ α₁≈β₁ α₂≈β₂
+      }
diff --git a/Functor/Instance/CMonoidalize.agda b/Functor/Instance/CMonoidalize.agda
new file mode 100644
index 0000000..41eb4e4
--- /dev/null
+++ b/Functor/Instance/CMonoidalize.agda
@@ -0,0 +1,42 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+open import Categories.Category using (Category)
+open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
+open import Categories.Category.Cocartesian using (Cocartesian)
+
+module Functor.Instance.CMonoidalize
+    {o o′ ℓ ℓ′ e e ′ : Level}
+    {C : Category o ℓ e}
+    (cocartesian : Cocartesian C)
+    (D : SymmetricMonoidalCategory o ℓ e)
+  where
+
+open import Categories.Category.Cocartesian using (module CocartesianSymmetricMonoidal)
+open import Categories.Functor using (Functor)
+open import Category.Construction.CMonoids using (CMonoids)
+open import Categories.Category.Construction.Functors using (Functors)
+open import Category.Construction.SymmetricMonoidalFunctors using (module Lax)
+open import Functor.Monoidal.Construction.CMonoidValued cocartesian {D} using () renaming (F,⊗,ε,σ to SMFOf)
+open import NaturalTransformation.Monoidal.Construction.CMonoidValued cocartesian {D} using () renaming (β,⊗,ε,σ to SMNTOf)
+
+private
+
+  open CocartesianSymmetricMonoidal C cocartesian
+
+  C-SMC : SymmetricMonoidalCategory o ℓ e
+  C-SMC = record { symmetric = +-symmetric }
+
+  module C = SymmetricMonoidalCategory C-SMC
+  module D = SymmetricMonoidalCategory D
+
+open Functor
+
+CMonoidalize : Functor (Functors C.U (CMonoids D.symmetric)) (Lax.SymmetricMonoidalFunctors C-SMC D)
+CMonoidalize .F₀ = SMFOf
+CMonoidalize .F₁ α = SMNTOf α
+CMonoidalize .identity = D.Equiv.refl
+CMonoidalize .homomorphism = D.Equiv.refl
+CMonoidalize .F-resp-≈ x = x
+
+module CMonoidalize = Functor CMonoidalize
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,⊗,ε,σ
diff --git a/NaturalTransformation/Monoidal/Construction/CMonoidValued.agda b/NaturalTransformation/Monoidal/Construction/CMonoidValued.agda
new file mode 100644
index 0000000..3005ee7
--- /dev/null
+++ b/NaturalTransformation/Monoidal/Construction/CMonoidValued.agda
@@ -0,0 +1,61 @@
+{-# 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 Categories.NaturalTransformation using (NaturalTransformation; _∘ˡ_)
+open import Level using (Level)
+
+-- A natural transformation between functors F, G
+-- from a cocartesian category 𝒞 to CMonoids[S]
+-- can be turned into a symmetric monoidal natural transformation
+-- between symmetric monoidal functors F′ G′ from 𝒞 to S
+
+module NaturalTransformation.Monoidal.Construction.CMonoidValued
+    {o o′ ℓ ℓ′ e e′ : Level}
+    {𝒞 : Category o ℓ e}
+    (𝒞-+ : Cocartesian 𝒞)
+    {S : SymmetricMonoidalCategory o′ ℓ′ e′}
+    (let module S = SymmetricMonoidalCategory S)
+    {M N : Functor 𝒞 (CMonoids S.symmetric)}
+    (α : NaturalTransformation M N)
+  where
+
+import Functor.Monoidal.Construction.CMonoidValued 𝒞-+ {S = S} as FamilyOfCMonoids
+import NaturalTransformation.Monoidal.Construction.MonoidValued as MonoidValued
+
+open import Categories.Category.Construction.Monoids using (Monoids)
+open import Functor.Forgetful.Instance.CMonoid S.symmetric using (Forget)
+
+module _ where
+  open import Categories.NaturalTransformation.Monoidal using (module Lax)
+  open Lax using (MonoidalNaturalTransformation) public
+
+module _ where
+  open import Categories.NaturalTransformation.Monoidal.Symmetric using (module Lax)
+  open Lax using (SymmetricMonoidalNaturalTransformation) public
+
+private
+
+  module M = Functor M
+  module N = Functor N
+  open FamilyOfCMonoids M using (F,⊗,ε,σ)
+  open FamilyOfCMonoids N using () renaming (F,⊗,ε,σ to G,⊗,ε,σ)
+
+  F : Functor 𝒞 (Monoids S.monoidal)
+  F = Forget ∙ M
+
+  G : Functor 𝒞 (Monoids S.monoidal)
+  G = Forget ∙ N
+
+  β : NaturalTransformation F G
+  β = Forget ∘ˡ α
+
+open MonoidValued 𝒞-+ β using (β,⊗,ε)
+
+β,⊗,ε,σ : SymmetricMonoidalNaturalTransformation F,⊗,ε,σ G,⊗,ε,σ
+β,⊗,ε,σ = record { MonoidalNaturalTransformation β,⊗,ε }
+
+module β,⊗,ε,σ = SymmetricMonoidalNaturalTransformation β,⊗,ε,σ