Category/Monoidal/Coherence.agda


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

{-# OPTIONS --without-K --safe #-}

open import Categories.Category.Core using (Category)
open import Categories.Category.Monoidal.Core using (Monoidal)

module Category.Monoidal.Coherence {o ℓ e} {𝒞 : Category o ℓ e} (monoidal : Monoidal 𝒞) where

import Categories.Morphism as Morphism
import Categories.Morphism.IsoEquiv as IsoEquiv
import Categories.Morphism.Reasoning as ⇒-Reasoning
import Categories.Category.Monoidal.Reasoning as ⊗-Reasoning

open import Categories.Functor.Properties using ([_]-resp-≅)

open Monoidal monoidal
open Category 𝒞

open ⇒-Reasoning 𝒞
open ⊗-Reasoning monoidal
open Morphism 𝒞 using (_≅_)
open IsoEquiv 𝒞 using (to-unique)

open Equiv

𝟏 : Obj
𝟏 = unit

module α≅ = associator
module λ≅ = unitorˡ
module ρ≅ = unitorʳ

private
  variable
    A B C D : Obj

α⇒ : (A ⊗₀ B) ⊗₀ C ⇒ A ⊗₀ B ⊗₀ C
α⇒ = α≅.from

α⇐ : A ⊗₀ B ⊗₀ C ⇒ (A ⊗₀ B) ⊗₀ C
α⇐ = α≅.to

λ⇒ : 𝟏 ⊗₀ A ⇒ A
λ⇒ = λ≅.from

λ⇐ : A ⇒ 𝟏 ⊗₀ A
λ⇐ = λ≅.to

ρ⇒ : A ⊗₀ 𝟏 ⇒ A
ρ⇒ = ρ≅.from

ρ⇐ : A ⇒ A ⊗₀ 𝟏
ρ⇐ = ρ≅.to

α⊗id : ((A ⊗₀ B) ⊗₀ C) ⊗₀ D ≅ (A ⊗₀ B ⊗₀ C) ⊗₀ D
α⊗id {A} {B} {C} {D} = [ -⊗ D ]-resp-≅ (associator {A} {B} {C})

module α⊗id {A} {B} {C} {D} = _≅_ (α⊗id {A} {B} {C} {D})

perimeter
    : α⇒ {𝟏} {A} {B} ∘ (ρ⇒ {𝟏} ⊗₁ id {A}) ⊗₁ id {B}
    ≈ id {𝟏} ⊗₁ λ⇒ {A ⊗₀ B} ∘ id {𝟏} ⊗₁ α⇒ {𝟏} {A} {B} ∘ α⇒ {𝟏} {𝟏 ⊗₀ A} {B} ∘ α⇒ {𝟏} {𝟏} {A} ⊗₁ id {B}
perimeter = begin
    α⇒ ∘ (ρ⇒ ⊗₁ id) ⊗₁ id               ≈⟨ assoc-commute-from ⟩
    ρ⇒ ⊗₁ id ⊗₁ id ∘ α⇒                 ≈⟨ refl⟩⊗⟨ ⊗.identity ⟩∘⟨refl ⟩
    ρ⇒ ⊗₁ id ∘ α⇒                       ≈⟨ pullˡ triangle ⟨
    id ⊗₁ λ⇒ ∘ α⇒ ∘ α⇒                  ≈⟨ refl⟩∘⟨ pentagon ⟨
    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ α⇒ ∘ α⇒ ⊗₁ id ∎

perimeter-triangle
    : α⇒ {𝟏} {A} {C} ∘ (id {𝟏} ⊗₁ λ⇒ {A}) ⊗₁ id {C}
    ≈ id {𝟏} ⊗₁ λ⇒ {A ⊗₀ C} ∘ id {𝟏} ⊗₁ α⇒ {𝟏} {A} {C} ∘ α⇒ {𝟏} {𝟏 ⊗₀ A} {C}
perimeter-triangle = begin
    α⇒ ∘ (id ⊗₁ λ⇒) ⊗₁ id                            ≈⟨ refl⟩∘⟨ identityʳ ⟨
    α⇒ ∘ (id ⊗₁ λ⇒) ⊗₁ id ∘ id                       ≈⟨ refl⟩∘⟨ refl⟩∘⟨ α⊗id.isoʳ ⟨
    α⇒ ∘ (id ⊗₁ λ⇒) ⊗₁ id ∘ α⇒ ⊗₁ id ∘ α⇐ ⊗₁ id      ≈⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟨
    α⇒ ∘ (id ⊗₁ λ⇒ ∘ α⇒) ⊗₁ id ∘ α⇐ ⊗₁ id            ≈⟨ refl⟩∘⟨ triangle ⟩⊗⟨refl ⟩∘⟨refl ⟩
    α⇒ ∘ (ρ⇒ ⊗₁ id) ⊗₁ id ∘ α⇐ ⊗₁ id                 ≈⟨ extendʳ perimeter ⟩
    id ⊗₁ λ⇒ ∘ (id ⊗₁ α⇒ ∘ α⇒ ∘ α⇒ ⊗₁ id) ∘ α⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ assoc ⟩
    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ (α⇒ ∘ α⇒ ⊗₁ id) ∘ α⇐ ⊗₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ assoc ⟩
    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ α⇒ ∘ α⇒ ⊗₁ id ∘ α⇐ ⊗₁ id   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ refl⟩∘⟨ α⊗id.isoʳ ⟩
    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ α⇒ ∘ id                    ≈⟨ refl⟩∘⟨ refl⟩∘⟨ identityʳ ⟩
    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ α⇒                         ∎

perimeter-triangle-square
    : ∀ {A C : Obj}
    → id {𝟏} ⊗₁ λ⇒ {A} ⊗₁ id {C}
    ≈ id {𝟏} ⊗₁ λ⇒ {A ⊗₀ C} ∘ id {𝟏} ⊗₁ α⇒ {𝟏} {A} {C}
perimeter-triangle-square = begin
    id ⊗₁ λ⇒ ⊗₁ id                  ≈⟨ identityʳ ⟨
    id ⊗₁ λ⇒ ⊗₁ id ∘ id             ≈⟨ refl⟩∘⟨ associator.isoʳ ⟨
    id ⊗₁ λ⇒ ⊗₁ id ∘ α⇒ ∘ α⇐        ≈⟨ extendʳ assoc-commute-from ⟨
    α⇒ ∘ (id ⊗₁ λ⇒) ⊗₁ id ∘ α⇐      ≈⟨ extendʳ perimeter-triangle ⟩
    id ⊗₁ λ⇒ ∘ (id ⊗₁ α⇒ ∘ α⇒) ∘ α⇐ ≈⟨ refl⟩∘⟨ assoc ⟩
    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ α⇒ ∘ α⇐   ≈⟨ refl⟩∘⟨ refl⟩∘⟨ associator.isoʳ ⟩
    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒ ∘ id        ≈⟨ refl⟩∘⟨ identityʳ ⟩
    id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒             ∎

λₕi≈λₕᵢ∘α₁ₕᵢ : λ⇒ {A} ⊗₁ id {C} ≈ λ⇒ {A ⊗₀ C} ∘ α⇒ {𝟏} {A} {C}
λₕi≈λₕᵢ∘α₁ₕᵢ = begin
    λ⇒ ⊗₁ id                          ≈⟨ insertʳ unitorˡ.isoʳ ⟩
    (λ⇒ ⊗₁ id ∘ λ⇒) ∘ λ⇐              ≈⟨ unitorˡ-commute-from ⟩∘⟨refl ⟨
    (λ⇒ ∘ id ⊗₁ λ⇒ ⊗₁ id) ∘ λ⇐        ≈⟨ (refl⟩∘⟨ perimeter-triangle-square) ⟩∘⟨refl ⟩
    (λ⇒ ∘ id ⊗₁ λ⇒ ∘ id ⊗₁ α⇒) ∘ λ⇐   ≈⟨ (refl⟩∘⟨ merge₂ˡ) ⟩∘⟨refl ⟩
    (λ⇒ ∘ id ⊗₁ (λ⇒ ∘ α⇒)) ∘ λ⇐       ≈⟨ unitorˡ-commute-from ⟩∘⟨refl ⟩
    ((λ⇒ ∘ α⇒) ∘ λ⇒) ∘ λ⇐             ≈⟨ cancelʳ unitorˡ.isoʳ ⟩
    λ⇒ ∘ α⇒                           ∎

1λ₁≈λ₁₁ : id {𝟏} ⊗₁ λ⇒ {𝟏} ≈ λ⇒ {𝟏 ⊗₀ 𝟏}
1λ₁≈λ₁₁ = begin
    id ⊗₁ λ⇒            ≈⟨ insertˡ unitorˡ.isoˡ ⟩
    λ⇐ ∘ λ⇒ ∘ id ⊗₁ λ⇒  ≈⟨ refl⟩∘⟨ unitorˡ-commute-from ⟩
    λ⇐ ∘ λ⇒ ∘ λ⇒        ≈⟨ cancelˡ unitorˡ.isoˡ ⟩
    λ⇒                  ∎

λ₁𝟏≈ρ₁𝟏 : λ⇒ {𝟏} ⊗₁ id {𝟏} ≈ ρ⇒ {𝟏} ⊗₁ id {𝟏}
λ₁𝟏≈ρ₁𝟏 = begin
    λ⇒ ⊗₁ id      ≈⟨ λₕi≈λₕᵢ∘α₁ₕᵢ ⟩
    λ⇒ ∘ α⇒       ≈⟨ 1λ₁≈λ₁₁ ⟩∘⟨refl ⟨
    id ⊗₁ λ⇒ ∘ α⇒ ≈⟨ triangle ⟩
    ρ⇒ ⊗₁ id      ∎

λ₁≅ρ₁⇒ : λ⇒ {𝟏} ≈ ρ⇒ {𝟏}
λ₁≅ρ₁⇒ = begin
    λ⇒                    ≈⟨ insertʳ unitorʳ.isoʳ ⟩
    (λ⇒ ∘ ρ⇒) ∘ ρ⇐        ≈⟨ unitorʳ-commute-from ⟩∘⟨refl ⟨
    (ρ⇒ ∘ λ⇒ ⊗₁ id) ∘ ρ⇐  ≈⟨ (refl⟩∘⟨ λ₁𝟏≈ρ₁𝟏) ⟩∘⟨refl ⟩
    (ρ⇒ ∘ ρ⇒ ⊗₁ id) ∘ ρ⇐  ≈⟨ unitorʳ-commute-from ⟩∘⟨refl ⟩
    (ρ⇒ ∘ ρ⇒) ∘ ρ⇐        ≈⟨ cancelʳ unitorʳ.isoʳ ⟩
    ρ⇒                    ∎

λ₁≅ρ₁⇐ : λ⇐ {𝟏} ≈ ρ⇐ {𝟏}
λ₁≅ρ₁⇐ = to-unique λ≅.iso ρ≅.iso λ₁≅ρ₁⇒