blob: e4b136c35945db2306d3523a9fea41c153033326 (
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
|
{-# 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.Properties using (idF-SymmetricMonoidal; ∘-SymmetricMonoidal)
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 }
}
|
