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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
{-# OPTIONS --without-K --safe #-}
open import Categories.Category using (Category)
open import Categories.Category.Cocartesian using (Cocartesian)
open import Category.Construction.CMonoids using (CMonoids)
open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
open import Categories.Functor using (Functor) renaming (_∘F_ to _∙_)
open import Categories.NaturalTransformation using (NaturalTransformation; _∘ˡ_)
open import Level using (Level)
-- A natural transformation between functors F, G
-- from a cocartesian category 𝒞 to CMonoids[S]
-- can be turned into a symmetric monoidal natural transformation
-- between symmetric monoidal functors F′ G′ from 𝒞 to S
module NaturalTransformation.Monoidal.Construction.CMonoidValued
{o o′ ℓ ℓ′ e e′ : Level}
{𝒞 : Category o ℓ e}
(𝒞-+ : Cocartesian 𝒞)
{S : SymmetricMonoidalCategory o′ ℓ′ e′}
(let module S = SymmetricMonoidalCategory S)
{M N : Functor 𝒞 (CMonoids S.symmetric)}
(α : NaturalTransformation M N)
where
import Functor.Monoidal.Construction.CMonoidValued 𝒞-+ {S = S} as FamilyOfCMonoids
import NaturalTransformation.Monoidal.Construction.MonoidValued as MonoidValued
open import Categories.Category.Construction.Monoids using (Monoids)
open import Functor.Forgetful.Instance.CMonoid S.symmetric using (Forget)
module _ where
open import Categories.NaturalTransformation.Monoidal using (module Lax)
open Lax using (MonoidalNaturalTransformation) public
module _ where
open import Categories.NaturalTransformation.Monoidal.Symmetric using (module Lax)
open Lax using (SymmetricMonoidalNaturalTransformation) public
private
module M = Functor M
module N = Functor N
open FamilyOfCMonoids M using (F,⊗,ε,σ)
open FamilyOfCMonoids N using () renaming (F,⊗,ε,σ to G,⊗,ε,σ)
F : Functor 𝒞 (Monoids S.monoidal)
F = Forget ∙ M
G : Functor 𝒞 (Monoids S.monoidal)
G = Forget ∙ N
β : NaturalTransformation F G
β = Forget ∘ˡ α
open MonoidValued 𝒞-+ β using (β,⊗,ε)
β,⊗,ε,σ : SymmetricMonoidalNaturalTransformation F,⊗,ε,σ G,⊗,ε,σ
β,⊗,ε,σ = record { MonoidalNaturalTransformation β,⊗,ε }
module β,⊗,ε,σ = SymmetricMonoidalNaturalTransformation β,⊗,ε,σ
|
