blob: 6423109bf09402ab6f6b801180b06e5c230fa894 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
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
|
