blob: 41eb4e415e7453f6d1b6562c2d92f09202950fb0 (
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
|
{-# 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
|
