blob: f4774b46bd793a9a7749eecc3da6547871e46569 (
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
|
{-# OPTIONS --without-K --safe #-}
open import Level using (Level)
open import Categories.Category.Monoidal using (MonoidalCategory)
open import Categories.Functor.Monoidal using (StrongMonoidalFunctor)
module Functor.Monoidal.Strong.Properties
{o o′ ℓ ℓ′ e e′ : Level}
{C : MonoidalCategory o ℓ e}
{D : MonoidalCategory o′ ℓ′ e′}
(F,φ,ε : StrongMonoidalFunctor C D) where
import Categories.Category.Monoidal.Utilities as ⊗-Utilities
import Categories.Category.Construction.Core as Core
open import Categories.Functor.Monoidal using (StrongMonoidalFunctor)
open import Categories.Functor.Properties using ([_]-resp-≅)
module C where
open MonoidalCategory C public
open ⊗-Utilities.Shorthands monoidal public using (α⇐; λ⇐; ρ⇐)
module D where
open MonoidalCategory D public
open ⊗-Utilities.Shorthands monoidal using (α⇐; λ⇐; ρ⇐) public
open Core.Shorthands U using (_∘ᵢ_; idᵢ; _≈ᵢ_; ⌞_⌟; to-≈; _≅_; module HomReasoningᵢ) public
open ⊗-Utilities monoidal using (_⊗ᵢ_) public
open D
open StrongMonoidalFunctor F,φ,ε
private
variable
X Y Z : C.Obj
Fα : F₀ ((X C.⊗₀ Y) C.⊗₀ Z) ≅ F₀ (X C.⊗₀ (Y C.⊗₀ Z))
Fα = [ F ]-resp-≅ C.associator
α : {A B C : Obj} → (A ⊗₀ B) ⊗₀ C ≅ A ⊗₀ (B ⊗₀ C)
α = associator
λ- : {A : Obj} → unit ⊗₀ A ≅ A
λ- = unitorˡ
Fλ : F₀ (C.unit C.⊗₀ X) ≅ F₀ X
Fλ = [ F ]-resp-≅ C.unitorˡ
ρ : {A : Obj} → A ⊗₀ unit ≅ A
ρ = unitorʳ
Fρ : F₀ (X C.⊗₀ C.unit) ≅ F₀ X
Fρ = [ F ]-resp-≅ C.unitorʳ
φ : F₀ X ⊗₀ F₀ Y ≅ F₀ (X C.⊗₀ Y)
φ = ⊗-homo.FX≅GX
module Shorthands where
φ⇒ : F₀ X ⊗₀ F₀ Y ⇒ F₀ (X C.⊗₀ Y)
φ⇒ = ⊗-homo.⇒.η _
φ⇐ : F₀ (X C.⊗₀ Y) ⇒ F₀ X ⊗₀ F₀ Y
φ⇐ = ⊗-homo.⇐.η _
ε⇒ : unit ⇒ F₀ C.unit
ε⇒ = ε.from
ε⇐ : F₀ C.unit ⇒ unit
ε⇐ = ε.to
open Shorthands
open HomReasoning
associativityᵢ : Fα {X} {Y} {Z} ∘ᵢ φ ∘ᵢ φ ⊗ᵢ idᵢ ≈ᵢ φ ∘ᵢ idᵢ ⊗ᵢ φ ∘ᵢ α
associativityᵢ = ⌞ associativity ⌟
associativity-inv : φ⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ (C.α⇐ {X} {Y} {Z}) ≈ α⇐ ∘ id ⊗₁ φ⇐ ∘ φ⇐
associativity-inv = begin
φ⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ C.α⇐ ≈⟨ sym-assoc ⟩
(φ⇐ ⊗₁ id ∘ φ⇐) ∘ F₁ C.α⇐ ≈⟨ to-≈ associativityᵢ ⟩
(α⇐ ∘ id ⊗₁ φ⇐) ∘ φ⇐ ≈⟨ assoc ⟩
α⇐ ∘ id ⊗₁ φ⇐ ∘ φ⇐ ∎
unitaryˡᵢ : Fλ {X} ∘ᵢ φ ∘ᵢ ε ⊗ᵢ idᵢ ≈ᵢ λ-
unitaryˡᵢ = ⌞ unitaryˡ ⌟
unitaryˡ-inv : ε⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ (C.λ⇐ {X}) ≈ λ⇐
unitaryˡ-inv = begin
ε⇐ ⊗₁ id ∘ φ⇐ ∘ F₁ C.λ⇐ ≈⟨ sym-assoc ⟩
(ε⇐ ⊗₁ id ∘ φ⇐) ∘ F₁ C.λ⇐ ≈⟨ to-≈ unitaryˡᵢ ⟩
λ⇐ ∎
unitaryʳᵢ : Fρ {X} ∘ᵢ φ ∘ᵢ idᵢ ⊗ᵢ ε ≈ᵢ ρ
unitaryʳᵢ = ⌞ unitaryʳ ⌟
unitaryʳ-inv : id ⊗₁ ε⇐ ∘ φ⇐ ∘ F₁ (C.ρ⇐ {X}) ≈ ρ⇐
unitaryʳ-inv = begin
id ⊗₁ ε⇐ ∘ φ⇐ ∘ F₁ C.ρ⇐ ≈⟨ sym-assoc ⟩
(id ⊗₁ ε⇐ ∘ φ⇐) ∘ F₁ C.ρ⇐ ≈⟨ to-≈ unitaryʳᵢ ⟩
ρ⇐ ∎
|
