Skip to content

Commit e279398

Browse files
JacquesCaretteJacquesCarette
authored
Merge pull request #272 from sstucki/braided-monoidal-functor
Add definition of braided monoidal functors...
2 parents 47d8bcb + ad6ba23 commit e279398

File tree

3 files changed

+125
-70
lines changed

3 files changed

+125
-70
lines changed

‎Everything.agda‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -276,6 +276,7 @@ import Categories.Functor.Instance.StrictCore
276276
import Categories.Functor.Instance.Twisted
277277
import Categories.Functor.Limits
278278
import Categories.Functor.Monoidal
279+
import Categories.Functor.Monoidal.Braided
279280
import Categories.Functor.Monoidal.Properties
280281
import Categories.Functor.Monoidal.Symmetric
281282
import Categories.Functor.Power

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

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
{-# OPTIONS --without-K --safe #-}
2+
3+
open import Categories.Category.Monoidal.Structure
4+
using (BraidedMonoidalCategory)
5+
6+
module Categories.Functor.Monoidal.Braided {o o′ ℓ ℓ′ e e′}
7+
(C : BraidedMonoidalCategory o ℓ e) (D : BraidedMonoidalCategory o′ ℓ′ e′)
8+
where
9+
10+
open import Level
11+
open import Data.Product using (_,_)
12+
13+
open import Categories.Category using (module Commutation)
14+
open import Categories.Functor using (Functor)
15+
open import Categories.Functor.Monoidal
16+
open import Categories.NaturalTransformation.NaturalIsomorphism
17+
using (NaturalIsomorphism)
18+
19+
open NaturalIsomorphism
20+
21+
private
22+
module C = BraidedMonoidalCategory C
23+
module D = BraidedMonoidalCategory D
24+
25+
module Lax where
26+
27+
-- Lax braided monoidal functors.
28+
29+
record IsBraidedMonoidalFunctor (F : Functor C.U D.U)
30+
: Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
31+
open Functor F
32+
33+
field
34+
isMonoidal : IsMonoidalFunctor C.monoidalCategory D.monoidalCategory F
35+
36+
open IsMonoidalFunctor isMonoidal public
37+
open D
38+
open Commutation D.U
39+
40+
-- coherence condition
41+
42+
field
43+
braiding-compat : ∀ {X Y} →
44+
[ F₀ X ⊗₀ F₀ Y ⇒ F₀ (Y C.⊗₀ X) ]⟨
45+
⊗-homo.η (X , Y) ⇒⟨ F₀ (X C.⊗₀ Y) ⟩
46+
F₁ (C.braiding.⇒.η (X , Y))
47+
≈ D.braiding.⇒.η (F₀ X , F₀ Y) ⇒⟨ F₀ Y ⊗₀ F₀ X ⟩
48+
⊗-homo.η (Y , X)
49+
⟩
50+
51+
record BraidedMonoidalFunctor : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
52+
field
53+
F : Functor C.U D.U
54+
isBraidedMonoidal : IsBraidedMonoidalFunctor F
55+
56+
open Functor F public
57+
open IsBraidedMonoidalFunctor isBraidedMonoidal public
58+
59+
monoidalFunctor : MonoidalFunctor C.monoidalCategory D.monoidalCategory
60+
monoidalFunctor = record { isMonoidal = isMonoidal }
61+
62+
module Strong where
63+
64+
-- Strong braided monoidal functors.
65+
66+
record IsBraidedMonoidalFunctor (F : Functor C.U D.U)
67+
: Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
68+
open Functor F
69+
70+
field
71+
isStrongMonoidal : IsStrongMonoidalFunctor C.monoidalCategory
72+
D.monoidalCategory F
73+
74+
open IsStrongMonoidalFunctor isStrongMonoidal public
75+
open D
76+
open Commutation D.U
77+
78+
-- coherence condition
79+
80+
field
81+
braiding-compat : ∀ {X Y} →
82+
[ F₀ X ⊗₀ F₀ Y ⇒ F₀ (Y C.⊗₀ X) ]⟨
83+
⊗-homo.⇒.η (X , Y) ⇒⟨ F₀ (X C.⊗₀ Y) ⟩
84+
F₁ (C.braiding.⇒.η (X , Y))
85+
≈ D.braiding.⇒.η (F₀ X , F₀ Y) ⇒⟨ F₀ Y ⊗₀ F₀ X ⟩
86+
⊗-homo.⇒.η (Y , X)
87+
⟩
88+
89+
isLaxBraidedMonoidal : Lax.IsBraidedMonoidalFunctor F
90+
isLaxBraidedMonoidal = record
91+
{ isMonoidal = isMonoidal
92+
; braiding-compat = braiding-compat
93+
}
94+
95+
record BraidedMonoidalFunctor : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
96+
field
97+
F : Functor C.U D.U
98+
isBraidedMonoidal : IsBraidedMonoidalFunctor F
99+
100+
open Functor F public
101+
open IsBraidedMonoidalFunctor isBraidedMonoidal public
102+
103+
monoidalFunctor : StrongMonoidalFunctor C.monoidalCategory
104+
D.monoidalCategory
105+
monoidalFunctor = record { isStrongMonoidal = isStrongMonoidal }

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

Lines changed: 19 additions & 70 deletions
Original file line numberDiff line numberDiff line change
@@ -10,96 +10,45 @@ module Categories.Functor.Monoidal.Symmetric {o o′ ℓ ℓ′ e e′}
1010
open import Level
1111
open import Data.Product using (_,_)
1212

13-
open import Categories.Category using (module Commutation)
1413
open import Categories.Functor using (Functor)
1514
open import Categories.Functor.Monoidal
16-
open import Categories.NaturalTransformation.NaturalIsomorphism
17-
using (NaturalIsomorphism)
18-
19-
open NaturalIsomorphism
2015

2116
private
22-
module C = SymmetricMonoidalCategory C
23-
module D = SymmetricMonoidalCategory D
24-
25-
module Lax where
26-
27-
-- Lax symmetric monoidal functors.
17+
module C = SymmetricMonoidalCategory C renaming (braidedMonoidalCategory to B)
18+
module D = SymmetricMonoidalCategory D renaming (braidedMonoidalCategory to B)
2819

29-
record IsSymmetricMonoidalFunctor (F : Functor C.U D.U)
30-
: Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
31-
open Functor F
20+
import Categories.Functor.Monoidal.Braided C.B D.B as Braided
3221

33-
field
34-
isMonoidal : IsMonoidalFunctor C.monoidalCategory D.monoidalCategory F
35-
36-
open IsMonoidalFunctor isMonoidal public
37-
open D
38-
open Commutation D.U
39-
40-
-- coherence condition
22+
module Lax where
23+
open Braided.Lax
4124

42-
field
43-
braiding-compat : ∀ {X Y} →
44-
[ F₀ X ⊗₀ F₀ Y ⇒ F₀ (Y C.⊗₀ X) ]⟨
45-
⊗-homo.η (X , Y) ⇒⟨ F₀ (X C.⊗₀ Y) ⟩
46-
F₁ (C.braiding.⇒.η (X , Y))
47-
≈ D.braiding.⇒.η (F₀ X , F₀ Y) ⇒⟨ F₀ Y ⊗₀ F₀ X ⟩
48-
⊗-homo.η (Y , X)
49-
⟩
25+
-- Lax symmetric monoidal functors are just lax braided monoidal
26+
-- functors between symmetric monoidal categories.
5027

5128
record SymmetricMonoidalFunctor : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
5229
field
53-
F : Functor C.U D.U
54-
isSymmetricMonoidal : IsSymmetricMonoidalFunctor F
30+
F : Functor C.U D.U
31+
isBraidedMonoidal : IsBraidedMonoidalFunctor F
5532

5633
open Functor F public
57-
open IsSymmetricMonoidalFunctor isSymmetricMonoidal public
34+
open IsBraidedMonoidalFunctor isBraidedMonoidal public
5835

5936
monoidalFunctor : MonoidalFunctor C.monoidalCategory D.monoidalCategory
60-
monoidalFunctor = record { F = F ; isMonoidal = isMonoidal }
37+
monoidalFunctor = record { isMonoidal = isMonoidal }
6138

6239
module Strong where
40+
open Braided.Strong
6341

64-
-- Strong symmetric monoidal functors.
65-
66-
record IsSymmetricMonoidalFunctor (F : Functor C.U D.U)
67-
: Set (o ⊔ ℓ ⊔ ℓ′ ⊔ e′) where
68-
open Functor F
69-
70-
field
71-
isStrongMonoidal : IsStrongMonoidalFunctor C.monoidalCategory
72-
D.monoidalCategory F
73-
74-
open IsStrongMonoidalFunctor isStrongMonoidal public
75-
open D
76-
open Commutation D.U
77-
78-
-- coherence condition
79-
80-
field
81-
braiding-compat : ∀ {X Y} →
82-
[ F₀ X ⊗₀ F₀ Y ⇒ F₀ (Y C.⊗₀ X) ]⟨
83-
⊗-homo.⇒.η (X , Y) ⇒⟨ F₀ (X C.⊗₀ Y) ⟩
84-
F₁ (C.braiding.⇒.η (X , Y))
85-
≈ D.braiding.⇒.η (F₀ X , F₀ Y) ⇒⟨ F₀ Y ⊗₀ F₀ X ⟩
86-
⊗-homo.⇒.η (Y , X)
87-
⟩
88-
89-
isLaxSymmetricMonoidal : Lax.IsSymmetricMonoidalFunctor F
90-
isLaxSymmetricMonoidal = record
91-
{ isMonoidal = isMonoidal
92-
; braiding-compat = braiding-compat
93-
}
42+
-- Strong symmetric monoidal functors are just strong braided
43+
-- monoidal functors between symmetric monoidal categories.
9444

9545
record SymmetricMonoidalFunctor : Set (o ⊔ ℓ ⊔ e ⊔ o′ ⊔ ℓ′ ⊔ e′) where
9646
field
97-
F : Functor C.U D.U
98-
isSymmetricMonoidal : IsSymmetricMonoidalFunctor F
47+
F : Functor C.U D.U
48+
isBraidedMonoidal : IsBraidedMonoidalFunctor F
9949

10050
open Functor F public
101-
open IsSymmetricMonoidalFunctor isSymmetricMonoidal public
51+
open IsBraidedMonoidalFunctor isBraidedMonoidal public
10252

103-
monoidalFunctor : StrongMonoidalFunctor C.monoidalCategory
104-
D.monoidalCategory
105-
monoidalFunctor = record { F = F ; isStrongMonoidal = isStrongMonoidal }
53+
monoidalFunctor : StrongMonoidalFunctor C.monoidalCategory D.monoidalCategory
54+
monoidalFunctor = record { isStrongMonoidal = isStrongMonoidal }

0 commit comments

Comments
 (0)