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
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
|
{-# OPTIONS --without-K --safe #-}
open import Categories.Category using (Category)
open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Category.Cocartesian.Bundle using (CocartesianCategory)
open import Categories.Category.Construction.Monoids using (Monoids)
open import Categories.Category.Monoidal.Bundle using (MonoidalCategory)
open import Categories.Functor using (Functor) renaming (_∘F_ to _∙_)
open import Categories.NaturalTransformation using (NaturalTransformation; ntHelper; _∘ˡ_)
open import Level using (Level)
-- A natural transformation between functors F, G
-- from a cocartesian category 𝒞 to Monoids[S]
-- can be turned into a monoidal natural transformation
-- between monoidal functors F′ G′ from 𝒞 to S
module NaturalTransformation.Monoidal.Construction.FamilyOfMonoids
{o o′ ℓ ℓ′ e e′ : Level}
{𝒞 : Category o ℓ e}
{𝒞-+ : Cocartesian 𝒞}
{S : MonoidalCategory o′ ℓ′ e′}
(let module S = MonoidalCategory S)
(M N : Functor 𝒞 (Monoids S.monoidal))
(α : NaturalTransformation M N)
where
import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
import Categories.Morphism.Reasoning as ⇒-Reasoning
import Categories.Object.Monoid as MonoidObject
import Functor.Monoidal.Construction.FamilyOfMonoids 𝒞-+ {S = S} as FamilyOfMonoids
open import Categories.Category using (module Definitions)
open import Categories.Functor.Properties using ([_]-resp-square)
open import Categories.NaturalTransformation.Monoidal using (module Lax)
open import Data.Product using (_,_)
open import Functor.Forgetful.Instance.Monoid S using (Forget)
private
module α = NaturalTransformation α
module M = Functor M
module N = Functor N
module 𝒞 = CocartesianCategory (record { cocartesian = 𝒞-+ })
open 𝒞 using (⊥; i₁; i₂; _+_)
open S
open MonoidObject monoidal using (Monoid; Monoid⇒)
open Definitions U using (CommutativeSquare)
open FamilyOfMonoids M using (F,⊗,ε)
open FamilyOfMonoids N using () renaming (F,⊗,ε to G,⊗,ε)
open Monoid using (μ; η)
open Monoid⇒
open ⇒-Reasoning U using (glue′)
open ⊗-Reasoning monoidal
F : Functor 𝒞 U
F = Forget ∙ M
G : Functor 𝒞 U
G = Forget ∙ N
β : NaturalTransformation F G
β = Forget ∘ˡ α
module F = Functor F
module G = Functor G
module β = NaturalTransformation β
module _ {A : 𝒞.Obj} where
εₘ : unit ⇒ F.₀ A
εₘ = η (M.₀ A)
⊲ₘ : F.₀ A ⊗₀ F.₀ A ⇒ F.₀ A
⊲ₘ = μ (M.₀ A)
εₙ : unit ⇒ G.₀ A
εₙ = η (N.₀ A)
⊲ₙ : G.₀ A ⊗₀ G.₀ A ⇒ G.₀ A
⊲ₙ = μ (N.₀ A)
ε-compat : β.η ⊥ ∘ εₘ ≈ εₙ
ε-compat = preserves-η (α.η ⊥)
module _ {n m : 𝒞.Obj} where
square : CommutativeSquare ⊲ₘ (β.η (n + m) ⊗₁ β.η (n + m)) (β.η (n + m)) ⊲ₙ
square = preserves-μ (α.η (n + m))
comm₁ : CommutativeSquare (F.₁ i₁) (β.η n) (β.η (n + m)) (G.₁ i₁)
comm₁ = β.commute i₁
comm₂ : CommutativeSquare (F.₁ i₂) (β.η m) (β.η (n + m)) (G.₁ i₂)
comm₂ = β.commute i₂
⊗-homo-compat : CommutativeSquare (⊲ₘ ∘ F.₁ i₁ ⊗₁ F.₁ i₂) (β.η n ⊗₁ β.η m) (β.η (n + m)) (⊲ₙ ∘ G.₁ i₁ ⊗₁ G.₁ i₂)
⊗-homo-compat = glue′ square (parallel comm₁ comm₂)
open Lax.MonoidalNaturalTransformation hiding (ε-compat; ⊗-homo-compat)
β,⊗,ε : Lax.MonoidalNaturalTransformation F,⊗,ε G,⊗,ε
β,⊗,ε .U = β
β,⊗,ε .isMonoidal = record
{ ε-compat = ε-compat
; ⊗-homo-compat = ⊗-homo-compat
}
module β,⊗,ε = Lax.MonoidalNaturalTransformation β,⊗,ε
|
