2 files changed, 45 insertions, 2 deletions
diff --git a/Functor/Instance/Monoidalize.agda b/Functor/Instance/Monoidalize.agda
new file mode 100644
index 0000000..6423109
--- /dev/null
+++ b/Functor/Instance/Monoidalize.agda
@@ -0,0 +1,43 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+open import Categories.Category using (Category)
+open import Categories.Category.Monoidal using (MonoidalCategory)
+open import Categories.Category.Cocartesian using (Cocartesian)
+
+module Functor.Instance.Monoidalize
+    {o o′ ℓ ℓ′ e e ′ : Level}
+    {C : Category o ℓ e}
+    (cocartesian : Cocartesian C)
+    (D : MonoidalCategory o ℓ e)
+  where
+
+open import Categories.Category.Cocartesian using (module CocartesianMonoidal)
+
+open import Categories.Functor using (Functor)
+open import Categories.Functor.Monoidal using (MonoidalFunctor)
+open import Categories.Category.Construction.Monoids using (Monoids)
+open import Categories.Category.Construction.Functors using (Functors)
+open import Categories.Category.Construction.MonoidalFunctors using (module Lax)
+open import Functor.Monoidal.Construction.MonoidValued cocartesian {D} using () renaming (F,⊗,ε to MonoidalFunctorOf)
+open import NaturalTransformation.Monoidal.Construction.MonoidValued cocartesian {D} using () renaming (β,⊗,ε to MonoidalNaturalTransformationOf)
+
+C-MC : MonoidalCategory o ℓ e
+C-MC = record { monoidal = +-monoidal }
+  where
+    open CocartesianMonoidal C cocartesian
+
+module C = MonoidalCategory C-MC
+module D = MonoidalCategory D
+
+open Lax using (MonoidalFunctors)
+open Functor
+
+Monoidalize : Functor (Functors C.U (Monoids D.monoidal)) (MonoidalFunctors C-MC D)
+Monoidalize .F₀ = MonoidalFunctorOf
+Monoidalize .F₁ α = MonoidalNaturalTransformationOf α
+Monoidalize .identity = D.Equiv.refl
+Monoidalize .homomorphism = D.Equiv.refl
+Monoidalize .F-resp-≈ x = x
+
+module Monoidalize = Functor Monoidalize
diff --git a/Functor/Monoidal/Construction/FamilyOfMonoids.agda b/Functor/Monoidal/Construction/MonoidValued.agda
index 377342a..937714d 100644
--- a/Functor/Monoidal/Construction/FamilyOfMonoids.agda
+++ b/Functor/Monoidal/Construction/MonoidValued.agda
@@ -11,7 +11,7 @@ open import Level using (Level; _⊔_)
 -- A functor from a cocartesian category 𝒞 to Monoids[S]
 -- can be turned into a monoidal functor from 𝒞 to S
 
-module Functor.Monoidal.Construction.FamilyOfMonoids
+module Functor.Monoidal.Construction.MonoidValued
     {o o′ ℓ ℓ′ e e′ : Level}
     {𝒞 : Category o ℓ e}
     (𝒞-+ : Cocartesian 𝒞)
@@ -33,7 +33,7 @@ open import Categories.Functor.Properties using ([_]-resp-square; [_]-resp-∘)
 open import Categories.Morphism using (_≅_)
 open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper)
 open import Data.Product using (_,_)
-open import Functor.Forgetful.Instance.Monoid S using (Forget)
+open import Functor.Forgetful.Instance.Monoid S.monoidal using (Forget)
 
 private