Skip to content

Commit 5fc0077

Browse files
JacquesCaretteJacquesCarette
authored
Merge pull request #283 from sstucki/sym-braid-nt-ni
Add support for braided/symmetric monoidal natural transformations/isomorphisms.
2 parents 184458d + 638e20b commit 5fc0077

File tree

6 files changed

+1058
-2
lines changed

6 files changed

+1058
-2
lines changed

‎Everything.agda‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -328,10 +328,14 @@ import Categories.NaturalTransformation.Equivalence
328328
import Categories.NaturalTransformation.Extranatural
329329
import Categories.NaturalTransformation.Hom
330330
import Categories.NaturalTransformation.Monoidal
331+
import Categories.NaturalTransformation.Monoidal.Braided
332+
import Categories.NaturalTransformation.Monoidal.Symmetric
331333
import Categories.NaturalTransformation.NaturalIsomorphism
332334
import Categories.NaturalTransformation.NaturalIsomorphism.Equivalence
333335
import Categories.NaturalTransformation.NaturalIsomorphism.Functors
334336
import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal
337+
import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Braided
338+
import Categories.NaturalTransformation.NaturalIsomorphism.Monoidal.Symmetric
335339
import Categories.NaturalTransformation.NaturalIsomorphism.Properties
336340
import Categories.NaturalTransformation.Properties
337341
import Categories.Object.Biproduct

‎src/Categories/Functor/Monoidal/Braided.agda‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ module Lax where
5050

5151
record BraidedMonoidalFunctor : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
5252
field
53-
F : Functor C.U D.U
53+
F : Functor C.U D.U
5454
isBraidedMonoidal : IsBraidedMonoidalFunctor F
5555

5656
open Functor F public
@@ -94,7 +94,7 @@ module Strong where
9494

9595
record BraidedMonoidalFunctor : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
9696
field
97-
F : Functor C.U D.U
97+
F : Functor C.U D.U
9898
isBraidedMonoidal : IsBraidedMonoidalFunctor F
9999

100100
open Functor F public

‎src/Categories/NaturalTransformation/Monoidal/Braided.agda‎

Lines changed: 194 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,194 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
-- Monoidal natural transformations between lax and strong braided
4+
-- monoidal functors.
5+
--
6+
-- NOTE. Braided monoidal natural transformations are really just
7+
-- monoidal natural transformations that happen to go between braided
8+
-- monoidal functors. No additional conditions are necessary.
9+
-- Nevertheless, the definitions in this module are useful when one is
10+
-- working in a braided monoidal setting. They also help Agda's type
11+
-- checker by bundling the (braided monoidal) categories and functors
12+
-- involved.
13+
--
14+
-- See
15+
-- * John Baez, Some definitions everyone should know,
16+
-- https://math.ucr.edu/home/baez/qg-fall2004/definitions.pdf
17+
-- * https://ncatlab.org/nlab/show/monoidal+natural+transformation
18+
19+
module Categories.NaturalTransformation.Monoidal.Braided where
20+
21+
open import Level
22+
23+
open import Categories.Category.Monoidal using (BraidedMonoidalCategory)
24+
import Categories.Functor.Monoidal.Braided as BMF
25+
open import Categories.Functor.Monoidal.Properties using ()
26+
renaming (∘-BraidedMonoidal to _∘Fˡ_; ∘-StrongBraidedMonoidal to _∘Fˢ_)
27+
open import Categories.NaturalTransformation as NT using (NaturalTransformation)
28+
import Categories.NaturalTransformation.Monoidal as MNT
29+
30+
module Lax where
31+
open BMF.Lax using (BraidedMonoidalFunctor)
32+
open MNT.Lax using (IsMonoidalNaturalTransformation)
33+
open BraidedMonoidalFunctor using () renaming (F to UF; monoidalFunctor to MF)
34+
35+
module _ {o ℓ e o′ ℓ′ e′}
36+
{C : BraidedMonoidalCategory o ℓ e}
37+
{D : BraidedMonoidalCategory o′ ℓ′ e′} where
38+
39+
-- Monoidal natural transformations between braided monoidal functors.
40+
41+
record BraidedMonoidalNaturalTransformation
42+
(F G : BraidedMonoidalFunctor C D) : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
43+
44+
field
45+
U : NaturalTransformation (UF F) (UF G)
46+
isMonoidal : IsMonoidalNaturalTransformation (MF F) (MF G) U
47+
48+
open NaturalTransformation U public
49+
open IsMonoidalNaturalTransformation isMonoidal public
50+
51+
-- To shorten some definitions
52+
53+
private
54+
_⇛_ = BraidedMonoidalNaturalTransformation
55+
module U = MNT.Lax
56+
57+
module _ {o ℓ e o′ ℓ′ e′}
58+
{C : BraidedMonoidalCategory o ℓ e}
59+
{D : BraidedMonoidalCategory o′ ℓ′ e′} where
60+
61+
-- Conversions
62+
63+
⌊_⌋ : {F G : BraidedMonoidalFunctor C D} →
64+
F ⇛ G → U.MonoidalNaturalTransformation (MF F) (MF G)
65+
⌊ α ⌋ = record { U = U ; isMonoidal = isMonoidal }
66+
where open BraidedMonoidalNaturalTransformation α
67+
68+
⌈_⌉ : {F G : BraidedMonoidalFunctor C D} →
69+
U.MonoidalNaturalTransformation (MF F) (MF G) → F ⇛ G
70+
⌈ α ⌉ = record { U = U ; isMonoidal = isMonoidal }
71+
where open U.MonoidalNaturalTransformation α
72+
73+
-- Identity and compositions
74+
75+
infixr 9 _∘ᵥ_
76+
77+
id : {F : BraidedMonoidalFunctor C D} → F ⇛ F
78+
id = ⌈ U.id ⌉
79+
80+
_∘ᵥ_ : {F G H : BraidedMonoidalFunctor C D} → G ⇛ H → F ⇛ G → F ⇛ H
81+
α ∘ᵥ β = ⌈ ⌊ α ⌋ U.∘ᵥ ⌊ β ⌋ ⌉
82+
83+
module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″}
84+
{C : BraidedMonoidalCategory o ℓ e}
85+
{D : BraidedMonoidalCategory o′ ℓ′ e′}
86+
{E : BraidedMonoidalCategory o″ ℓ″ e″} where
87+
88+
infixr 9 _∘ₕ_ _∘ˡ_ _∘ʳ_
89+
90+
_∘ₕ_ : {F G : BraidedMonoidalFunctor C D}
91+
{H I : BraidedMonoidalFunctor D E} →
92+
H ⇛ I → F ⇛ G → (H ∘Fˡ F) ⇛ (I ∘Fˡ G)
93+
α ∘ₕ β = ⌈ ⌊ α ⌋ U.∘ₕ ⌊ β ⌋ ⌉
94+
95+
_∘ˡ_ : {F G : BraidedMonoidalFunctor C D}
96+
(H : BraidedMonoidalFunctor D E) → F ⇛ G → (H ∘Fˡ F) ⇛ (H ∘Fˡ G)
97+
H ∘ˡ α = id {F = H} ∘ₕ α
98+
99+
_∘ʳ_ : {G H : BraidedMonoidalFunctor D E} →
100+
G ⇛ H → (F : BraidedMonoidalFunctor C D) → (G ∘Fˡ F) ⇛ (H ∘Fˡ F)
101+
α ∘ʳ F = α ∘ₕ id {F = F}
102+
103+
module Strong where
104+
open BMF.Strong using (BraidedMonoidalFunctor)
105+
open MNT.Strong using (IsMonoidalNaturalTransformation)
106+
open BraidedMonoidalFunctor using () renaming
107+
( F to UF
108+
; monoidalFunctor to MF
109+
; laxBraidedMonoidalFunctor to laxBMF
110+
)
111+
112+
module _ {o ℓ e o′ ℓ′ e′}
113+
{C : BraidedMonoidalCategory o ℓ e}
114+
{D : BraidedMonoidalCategory o′ ℓ′ e′} where
115+
116+
-- Monoidal natural transformations between braided strong
117+
-- monoidal functors.
118+
119+
record BraidedMonoidalNaturalTransformation
120+
(F G : BraidedMonoidalFunctor C D) : Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
121+
122+
field
123+
U : NaturalTransformation (UF F) (UF G)
124+
isMonoidal : IsMonoidalNaturalTransformation (MF F) (MF G) U
125+
126+
laxBNT : Lax.BraidedMonoidalNaturalTransformation (laxBMF F) (laxBMF G)
127+
laxBNT = record { U = U ; isMonoidal = isMonoidal }
128+
open Lax.BraidedMonoidalNaturalTransformation laxBNT public
129+
hiding (U; isMonoidal)
130+
131+
-- To shorten some definitions
132+
133+
private
134+
_⇛_ = BraidedMonoidalNaturalTransformation
135+
module U = MNT.Strong
136+
137+
module _ {o ℓ e o′ ℓ′ e′}
138+
{C : BraidedMonoidalCategory o ℓ e}
139+
{D : BraidedMonoidalCategory o′ ℓ′ e′} where
140+
141+
-- Conversions
142+
143+
⌊_⌋ : {F G : BraidedMonoidalFunctor C D} →
144+
F ⇛ G → U.MonoidalNaturalTransformation (MF F) (MF G)
145+
⌊ α ⌋ = record { U = U ; isMonoidal = isMonoidal }
146+
where open BraidedMonoidalNaturalTransformation α
147+
148+
⌈_⌉ : {F G : BraidedMonoidalFunctor C D} →
149+
U.MonoidalNaturalTransformation (MF F) (MF G) → F ⇛ G
150+
⌈ α ⌉ = record { U = U ; isMonoidal = isMonoidal }
151+
where open U.MonoidalNaturalTransformation α
152+
153+
-- Identity and compositions
154+
155+
infixr 9 _∘ᵥ_
156+
157+
id : {F : BraidedMonoidalFunctor C D} → F ⇛ F
158+
id = ⌈ U.id ⌉
159+
160+
_∘ᵥ_ : {F G H : BraidedMonoidalFunctor C D} → G ⇛ H → F ⇛ G → F ⇛ H
161+
α ∘ᵥ β = ⌈ ⌊ α ⌋ U.∘ᵥ ⌊ β ⌋ ⌉
162+
163+
module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″}
164+
{C : BraidedMonoidalCategory o ℓ e}
165+
{D : BraidedMonoidalCategory o′ ℓ′ e′}
166+
{E : BraidedMonoidalCategory o″ ℓ″ e″} where
167+
168+
infixr 9 _∘ₕ_ _∘ˡ_ _∘ʳ_
169+
170+
_∘ₕ_ : {F G : BraidedMonoidalFunctor C D}
171+
{H I : BraidedMonoidalFunctor D E} →
172+
H ⇛ I → F ⇛ G → (H ∘Fˢ F) ⇛ (I ∘Fˢ G)
173+
-- NOTE: this definition is clearly equivalent to
174+
--
175+
-- α ∘ₕ β = ⌈ ⌊ α ⌋ U.∘ₕ ⌊ β ⌋ ⌉
176+
--
177+
-- but the latter takes an unreasonably long time to typecheck,
178+
-- while the unfolded version typechecks almost immediately.
179+
α ∘ₕ β = record
180+
{ U = C.U
181+
; isMonoidal = record
182+
{ ε-compat = C.ε-compat
183+
; ⊗-homo-compat = C.⊗-homo-compat
184+
}
185+
}
186+
where module C = U.MonoidalNaturalTransformation (⌊ α ⌋ U.∘ₕ ⌊ β ⌋)
187+
188+
_∘ˡ_ : {F G : BraidedMonoidalFunctor C D}
189+
(H : BraidedMonoidalFunctor D E) → F ⇛ G → (H ∘Fˢ F) ⇛ (H ∘Fˢ G)
190+
H ∘ˡ α = id {F = H} ∘ₕ α
191+
192+
_∘ʳ_ : {G H : BraidedMonoidalFunctor D E} →
193+
G ⇛ H → (F : BraidedMonoidalFunctor C D) → (G ∘Fˢ F) ⇛ (H ∘Fˢ F)
194+
α ∘ʳ F = α ∘ₕ id {F = F}

0 commit comments

Comments
 (0)