1 files changed, 61 insertions, 0 deletions

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 β,⊗,ε,σ