Extend monoidalize functor to commutative monoids

1 files changed, 59 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-≈ α₁≈β₁ α₂≈β₂
+      }