blob: 669363992ebc69c9b639e48f2ef6f8b6b439a25b (
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
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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
{-# OPTIONS --without-K --safe #-}
{-# OPTIONS --lossy-unification #-}
open import Level using (Level; suc; _⊔_)
module Category.Instance.SymMonCat {o ℓ e : Level} where
import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning
import Categories.Functor.Monoidal.Symmetric as SMF
import Categories.Morphism.Reasoning as ⇒-Reasoning
import Categories.Morphism as Morphism
import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric as SMNI
import Categories.Category.Monoidal.Utilities as MonoidalUtil
import Categories.Category.Monoidal.Braided.Properties as BraidedProperties
open import Relation.Binary.Core using (Rel)
open import Categories.Category using (Category; _[_,_]; _[_∘_])
open import Categories.Category.Helper using (categoryHelper)
open import Categories.Category.Monoidal.Bundle using (SymmetricMonoidalCategory)
open import Categories.Functor.Monoidal.Symmetric.Properties using (idF-SymmetricMonoidal; idF-StrongSymmetricMonoidal; ∘-SymmetricMonoidal; ∘-StrongSymmetricMonoidal)
-- Category of symmetric monoidal categories and lax symmetric monoidal functors
module Lax where
open SMF.Lax using (SymmetricMonoidalFunctor)
open SMNI.Lax using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence)
assoc
: {A B C D : SymmetricMonoidalCategory o ℓ e}
{F : SymmetricMonoidalFunctor A B}
{G : SymmetricMonoidalFunctor B C}
{H : SymmetricMonoidalFunctor C D}
→ SymmetricMonoidalNaturalIsomorphism
(∘-SymmetricMonoidal (∘-SymmetricMonoidal H G) F)
(∘-SymmetricMonoidal H (∘-SymmetricMonoidal G F))
assoc {A} {B} {C} {D} {F} {G} {H} = SMNI.Lax.associator {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {D} {F} {G} {H}
identityˡ
: {A B : SymmetricMonoidalCategory o ℓ e}
{F : SymmetricMonoidalFunctor A B}
→ SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal (idF-SymmetricMonoidal B) F) F
identityˡ {A} {B} {F} = SMNI.Lax.unitorˡ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F}
identityʳ
: {A B : SymmetricMonoidalCategory o ℓ e}
{F : SymmetricMonoidalFunctor A B}
→ SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal F (idF-SymmetricMonoidal A)) F
identityʳ {A} {B} {F} = SMNI.Lax.unitorʳ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F}
Compose
: {A B C : SymmetricMonoidalCategory o ℓ e}
→ SymmetricMonoidalFunctor B C
→ SymmetricMonoidalFunctor A B
→ SymmetricMonoidalFunctor A C
Compose {A} {B} {C} F G = ∘-SymmetricMonoidal {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} F G
∘-resp-≈
: {A B C : SymmetricMonoidalCategory o ℓ e}
{f h : SymmetricMonoidalFunctor B C}
{g i : SymmetricMonoidalFunctor A B}
→ SymmetricMonoidalNaturalIsomorphism f h
→ SymmetricMonoidalNaturalIsomorphism g i
→ SymmetricMonoidalNaturalIsomorphism (∘-SymmetricMonoidal f g) (∘-SymmetricMonoidal h i)
∘-resp-≈ {A} {B} {C} {F} {F′} {G} {G′} F≃F′ G≃G′ = SMNI.Lax._ⓘₕ_ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {G} {G′} {F} {F′} F≃F′ G≃G′
SymMonCat : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
SymMonCat = categoryHelper record
{ Obj = SymmetricMonoidalCategory o ℓ e
; _⇒_ = SymmetricMonoidalFunctor {o} {o} {ℓ} {ℓ} {e} {e}
; _≈_ = λ { {A} {B} → SymmetricMonoidalNaturalIsomorphism {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} }
; id = λ { {X} → idF-SymmetricMonoidal X }
; _∘_ = λ { {A} {B} {C} F G → Compose {A} {B} {C} F G }
; assoc = λ { {A} {B} {C} {D} {F} {G} {H} → assoc {A} {B} {C} {D} {F} {G} {H} }
; identityˡ = λ { {A} {B} {F} → identityˡ {A} {B} {F} }
; identityʳ = λ { {A} {B} {F} → identityʳ {A} {B} {F} }
; equiv = isEquivalence
; ∘-resp-≈ = λ { {A} {B} {C} {f} {h} {g} {i} f≈h g≈i → ∘-resp-≈ {A} {B} {C} {f} {h} {g} {i} f≈h g≈i }
}
module Strong where
open SMF.Strong using (SymmetricMonoidalFunctor)
open SMNI.Strong using (SymmetricMonoidalNaturalIsomorphism; id; isEquivalence)
assoc
: {A B C D : SymmetricMonoidalCategory o ℓ e}
{F : SymmetricMonoidalFunctor A B}
{G : SymmetricMonoidalFunctor B C}
{H : SymmetricMonoidalFunctor C D}
→ SymmetricMonoidalNaturalIsomorphism
(∘-StrongSymmetricMonoidal (∘-StrongSymmetricMonoidal H G) F)
(∘-StrongSymmetricMonoidal H (∘-StrongSymmetricMonoidal G F))
assoc {A} {B} {C} {D} {F} {G} {H} = SMNI.Strong.associator {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {D} {F} {G} {H}
identityˡ
: {A B : SymmetricMonoidalCategory o ℓ e}
{F : SymmetricMonoidalFunctor A B}
→ SymmetricMonoidalNaturalIsomorphism (∘-StrongSymmetricMonoidal (idF-StrongSymmetricMonoidal B) F) F
identityˡ {A} {B} {F} = SMNI.Strong.unitorˡ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F}
identityʳ
: {A B : SymmetricMonoidalCategory o ℓ e}
{F : SymmetricMonoidalFunctor A B}
→ SymmetricMonoidalNaturalIsomorphism (∘-StrongSymmetricMonoidal F (idF-StrongSymmetricMonoidal A)) F
identityʳ {A} {B} {F} = SMNI.Strong.unitorʳ {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {F}
Compose
: {A B C : SymmetricMonoidalCategory o ℓ e}
→ SymmetricMonoidalFunctor B C
→ SymmetricMonoidalFunctor A B
→ SymmetricMonoidalFunctor A C
Compose {A} {B} {C} F G = ∘-StrongSymmetricMonoidal {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} F G
∘-resp-≈
: {A B C : SymmetricMonoidalCategory o ℓ e}
{f h : SymmetricMonoidalFunctor B C}
{g i : SymmetricMonoidalFunctor A B}
→ SymmetricMonoidalNaturalIsomorphism f h
→ SymmetricMonoidalNaturalIsomorphism g i
→ SymmetricMonoidalNaturalIsomorphism (∘-StrongSymmetricMonoidal f g) (∘-StrongSymmetricMonoidal h i)
∘-resp-≈ {A} {B} {C} {F} {F′} {G} {G′} F≃F′ G≃G′ = SMNI.Strong._ⓘₕ_ {o} {ℓ} {e} {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} {C} {G} {G′} {F} {F′} F≃F′ G≃G′
SymMonCat : Category (suc (o ⊔ ℓ ⊔ e)) (o ⊔ ℓ ⊔ e) (o ⊔ ℓ ⊔ e)
SymMonCat = categoryHelper record
{ Obj = SymmetricMonoidalCategory o ℓ e
; _⇒_ = SymmetricMonoidalFunctor {o} {o} {ℓ} {ℓ} {e} {e}
; _≈_ = λ { {A} {B} → SymmetricMonoidalNaturalIsomorphism {o} {ℓ} {e} {o} {ℓ} {e} {A} {B} }
; id = λ { {X} → idF-StrongSymmetricMonoidal X }
; _∘_ = λ { {A} {B} {C} F G → Compose {A} {B} {C} F G }
; assoc = λ { {A} {B} {C} {D} {F} {G} {H} → assoc {A} {B} {C} {D} {F} {G} {H} }
; identityˡ = λ { {A} {B} {F} → identityˡ {A} {B} {F} }
; identityʳ = λ { {A} {B} {F} → identityʳ {A} {B} {F} }
; equiv = isEquivalence
; ∘-resp-≈ = λ { {A} {B} {C} {f} {h} {g} {i} f≈h g≈i → ∘-resp-≈ {A} {B} {C} {f} {h} {g} {i} f≈h g≈i }
}
|
