diff options
Diffstat (limited to 'Functor/Instance')
| -rw-r--r-- | Functor/Instance/Monoidalize.agda | 43 |
1 files changed, 43 insertions, 0 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 |