From 3e0565657f896d3064e68b03d30c1a748a8bed25 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sat, 10 Jan 2026 22:04:30 -0600 Subject: Extend monoidalize functor to commutative monoids --- Functor/Instance/CMonoidalize.agda | 42 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 Functor/Instance/CMonoidalize.agda (limited to 'Functor/Instance') 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 -- cgit v1.2.3