From 8e40a6e427aea3cdfeda038c38942e9d66c502e3 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sat, 13 Dec 2025 20:37:32 -0600 Subject: Add Monoidalize functor --- Functor/Instance/Monoidalize.agda | 43 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 Functor/Instance/Monoidalize.agda (limited to 'Functor/Instance') 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 -- cgit v1.2.3