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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
|
{-# OPTIONS --without-K --safe #-}
open import Categories.Category using (Category)
open import Category.Dagger.Semiadditive using (SemiadditiveDagger)
open import Level using (Level)
module Data.WiringDiagram.Monoidal.Braided
{o ℓ e : Level}
{𝒞 : Category o ℓ e}
(S : SemiadditiveDagger 𝒞)
where
import Categories.Morphism.Reasoning 𝒞 as ⇒-Reasoning
import Data.WiringDiagram.Core as WD
open import Categories.Category.Monoidal using (Monoidal)
open import Categories.Category.Monoidal.Braided using (Braided)
open import Categories.Category.Monoidal.Braided.Properties using (hexagon₁-inv; hexagon₂-inv)
open import Categories.Category.Monoidal.Symmetric using (module Symmetric)
open import Categories.Functor.Bifunctor using (flip-bifunctor)
open import Categories.NaturalTransformation.NaturalIsomorphism using (_≃_; niHelper)
open import Data.Product using (uncurry; _,_)
open import Data.WiringDiagram.Monoidal.Core S
using (_⊞_; _⊞₁_; σ₂₃; associator⇒; associator⇐; DWD-Monoidal; BWD-Monoidal)
renaming (module Directed to D; module Balanced to B)
open import Function using (flip)
open Category 𝒞
open SemiadditiveDagger S
open Symmetric symmetric using (braided; hexagon₁; hexagon₂)
open WD S using (Box; WiringDiagram; _□_; _⧈_; _≈-⧈_; _⌸_; id-⧈; _⌻_; ≈-sym)
open HomReasoning
open ⇒-Reasoning
open Equiv
σ₂₃-⟨⟩
: {X A B C D : Obj}
{f : X ⇒ A}
{g : X ⇒ B}
{h : X ⇒ C}
{i : X ⇒ D}
→ σ₂₃ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ≈ ⟨ ⟨ f , h ⟩ , ⟨ g , i ⟩ ⟩
σ₂₃-⟨⟩ {f = f} {g} {h} {i} = begin
σ₂₃ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ≈⟨ ⟨⟩∘ ⟩
⟨ π₁ ×₁ π₁ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ , π₂ ×₁ π₂ ∘ ⟨ ⟨ f , g ⟩ , ⟨ h , i ⟩ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ ×₁∘⟨⟩ ×₁∘⟨⟩ ⟩
⟨ ⟨ π₁ ∘ ⟨ f , g ⟩ , π₁ ∘ ⟨ h , i ⟩ ⟩ , ⟨ π₂ ∘ ⟨ f , g ⟩ , π₂ ∘ ⟨ h , i ⟩ ⟩ ⟩ ≈⟨ ⟨⟩-cong₂ (⟨⟩-cong₂ project₁ project₁) (⟨⟩-cong₂ project₂ project₂) ⟩
⟨ ⟨ f , h ⟩ , ⟨ g , i ⟩ ⟩ ∎
swap-⧈ : (X Y : Box) → WiringDiagram (X ⊞ Y) (Y ⊞ X)
swap-⧈ X Y = swap ∘ π₂ ⧈ swap
swap-commute
: {X X′ Y Y′ : Box}
(f : WiringDiagram X X′)
(g : WiringDiagram Y Y′)
→ swap-⧈ X′ Y′ ⌻ f ⊞₁ g ≈-⧈ g ⊞₁ f ⌻ swap-⧈ X Y
swap-commute (fᵢ ⧈ fₒ) (gᵢ ⧈ gₒ) = eqᵢ ⌸ swap∘×₁
where
eqᵢ : (fᵢ ×₁ gᵢ ∘ σ₂₃) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ (fₒ ×₁ gₒ) ×₁ id ⟩ ≈ (swap ∘ π₂) ∘ ⟨ π₁ , (gᵢ ×₁ fᵢ ∘ σ₂₃) ∘ swap ×₁ id ⟩
eqᵢ = begin
(fᵢ ×₁ gᵢ ∘ σ₂₃) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ (fₒ ×₁ gₒ) ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullʳ π₂∘first) ⟩
(fᵢ ×₁ gᵢ ∘ σ₂₃) ∘ ⟨ π₁ , swap ∘ π₂ ⟩ ≈⟨ pullʳ ⟨⟩∘ ⟩
fᵢ ×₁ gᵢ ∘ ⟨ π₁ ×₁ π₁ ∘ _ , π₂ ×₁ π₂ ∘ ⟨ π₁ , swap ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ ×₁∘⟨⟩ ×₁∘⟨⟩ ⟩
fᵢ ×₁ gᵢ ∘ ⟨ ⟨ _ , _ ⟩ , ⟨ π₂ ∘ π₁ , π₂ ∘ swap ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-cong₂ (⟨⟩-congˡ (pullˡ project₁)) (⟨⟩-congˡ (pullˡ project₂)) ⟩
fᵢ ×₁ gᵢ ∘ ⟨ π₁ ×₁ π₂ , π₂ ×₁ π₁ ⟩ ≈⟨ refl⟩∘⟨ swap∘⟨⟩ ⟨
fᵢ ×₁ gᵢ ∘ swap ∘ ⟨ π₂ ×₁ π₁ , π₁ ×₁ π₂ ⟩ ≈⟨ refl⟩∘⟨ pushʳ (sym σ₂₃-⟨⟩) ⟩
fᵢ ×₁ gᵢ ∘ (swap ∘ σ₂₃) ∘ ⟨ _ , ⟨ π₁ ∘ π₂ , π₂ ∘ π₂ ⟩ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ ⟨⟩∘ ⟨⟩∘ ⟨
fᵢ ×₁ gᵢ ∘ (swap ∘ σ₂₃) ∘ ⟨ _ ∘ π₁ , ⟨ π₁ , π₂ ⟩ ∘ π₂ ⟩ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-congˡ (η ⟩∘⟨refl) ⟩
fᵢ ×₁ gᵢ ∘ (swap ∘ σ₂₃) ∘ swap ×₁ id ≈⟨ extendʳ (extendʳ swap∘×₁) ⟨
swap ∘ (gᵢ ×₁ fᵢ ∘ σ₂₃) ∘ swap ×₁ id ≈⟨ pushʳ (sym project₂) ⟩
(swap ∘ π₂) ∘ ⟨ π₁ , (gᵢ ×₁ fᵢ ∘ σ₂₃) ∘ swap ×₁ id ⟩ ∎
swap∘swap-⧈
: {X Y : Box}
→ swap-⧈ Y X ⌻ swap-⧈ X Y ≈-⧈ id-⧈
swap∘swap-⧈ = eqᵢ ⌸ swap∘swap
where
eqᵢ : (swap ∘ π₂) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ swap ×₁ id ⟩ ≈ π₂
eqᵢ = begin
(swap ∘ π₂) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ swap ×₁ id ⟩ ≈⟨ pullʳ project₂ ⟩
swap ∘ (swap ∘ π₂) ∘ swap ×₁ id ≈⟨ refl⟩∘⟨ pullʳ π₂∘first ⟩
swap ∘ swap ∘ π₂ ≈⟨ cancelˡ swap∘swap ⟩
π₂ ∎
hex₁
: {X Y Z : Box}
→ id-⧈ ⊞₁ swap-⧈ X Z ⌻ associator⇒ ⌻ swap-⧈ X Y ⊞₁ id-⧈ {Z}
≈-⧈ associator⇒ ⌻ swap-⧈ X (Y ⊞ Z) ⌻ associator⇒
hex₁ = eqᵢ ⌸ hexagon₁
where
eqᵢ : (((swap ∘ π₂) ×₁ π₂ ∘ σ₂₃) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ (swap ×₁ id) ×₁ id ⟩) ∘ ⟨ π₁ , (π₂ ×₁ (swap ∘ π₂) ∘ σ₂₃) ∘ (assocˡ ∘ swap ×₁ id) ×₁ id ⟩
≈ ((assocʳ ∘ π₂) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ assocˡ ×₁ id ⟩) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ (swap ∘ assocˡ) ×₁ id ⟩
eqᵢ = begin
(((swap ∘ π₂) ×₁ π₂ ∘ σ₂₃) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ (swap ×₁ id) ×₁ id ⟩) ∘ _ ≈⟨ (refl⟩∘⟨ ⟨⟩-congˡ (pullʳ π₂∘first)) ⟩∘⟨refl ⟩
(((swap ∘ π₂) ×₁ π₂ ∘ ⟨ π₁ ×₁ π₁ , π₂ ×₁ π₂ ⟩) ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _ ≈⟨ ×₁∘⟨⟩ ⟩∘⟨refl ⟩∘⟨refl ⟩
((⟨ (swap ∘ π₂) ∘ π₁ ×₁ π₁ , π₂ ∘ π₂ ×₁ π₂ ⟩) ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _ ≈⟨ ⟨⟩-cong₂ (extendˡ π₂∘×₁) π₂∘×₁ ⟩∘⟨refl ⟩∘⟨refl ⟩
((⟨ (swap ∘ π₁) ∘ π₂ , π₂ ∘ π₂ ⟩) ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _ ≈⟨ ⟨⟩∘ ⟩∘⟨refl ⟩∘⟨refl ⟨
((⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂) ∘ ⟨ π₁ , assocʳ ∘ π₂ ⟩) ∘ _ ≈⟨ pullʳ project₂ ⟩∘⟨refl ⟩
(⟨ swap ∘ π₁ , π₂ ⟩ ∘ assocʳ ∘ π₂) ∘ _ ≈⟨ pullʳ (pullʳ project₂) ⟩
⟨ swap ∘ π₁ , π₂ ⟩ ∘ assocʳ ∘ (π₂ ×₁ (swap ∘ π₂) ∘ σ₂₃) ∘ _ ×₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ×₁∘⟨⟩ ⟩∘⟨refl ⟩
⟨ _ ∘ π₁ , π₂ ⟩ ∘ _ ∘ ⟨ π₂ ∘ π₁ ×₁ π₁ , (swap ∘ π₂) ∘ π₂ ×₁ π₂ ⟩ ∘ _ ×₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ ⟨⟩-cong₂ π₂∘×₁ (extendˡ π₂∘×₁) ⟩∘⟨refl ⟩
⟨ swap ∘ π₁ , π₂ ⟩ ∘ assocʳ ∘ ⟨ π₁ ∘ π₂ , (swap ∘ π₂) ∘ π₂ ⟩ ∘ _ ×₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ (sym ⟨⟩∘) ⟩
⟨ swap ∘ π₁ , π₂ ⟩ ∘ assocʳ ∘ ⟨ π₁ , swap ∘ π₂ ⟩ ∘ π₂ ∘ _ ×₁ id ≈⟨ pushʳ (refl⟩∘⟨ refl⟩∘⟨ π₂∘first) ⟩
(⟨ swap ∘ π₁ , π₂ ⟩ ∘ assocʳ) ∘ ⟨ π₁ , swap ∘ π₂ ⟩ ∘ π₂ ≈⟨ (⟨⟩-congˡ identityˡ ⟩∘⟨refl) ⟩∘⟨ ⟨⟩-congʳ identityˡ ⟩∘⟨refl ⟨
(swap ×₁ id ∘ assocʳ) ∘ id ×₁ swap ∘ π₂ ≈⟨ extendʳ (hexagon₁-inv braided) ⟩
(assocʳ ∘ swap) ∘ assocʳ ∘ π₂ ≈⟨ refl⟩∘⟨ pushʳ (sym π₂∘first) ⟩
(assocʳ ∘ swap) ∘ (assocʳ ∘ π₂) ∘ _ ×₁ id ≈⟨ pushʳ (sym project₂) ⟩
((assocʳ ∘ swap) ∘ π₂) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ _ ×₁ id ⟩ ≈⟨ pullʳ (pushʳ (sym π₂∘first)) ⟩∘⟨refl ⟩
(assocʳ ∘ (swap ∘ π₂) ∘ assocˡ ×₁ id) ∘ ⟨ π₁ , (assocʳ ∘ π₂) ∘ _ ×₁ id ⟩ ≈⟨ pushʳ (sym project₂) ⟩∘⟨refl ⟩
((assocʳ ∘ π₂) ∘ ⟨ π₁ , (swap ∘ π₂) ∘ assocˡ ×₁ id ⟩) ∘ ⟨ π₁ , _ ∘ _ ×₁ id ⟩ ∎
hex₂
: {X Y Z : Box}
→ (swap-⧈ X Z ⊞₁ id-⧈ ⌻ associator⇐) ⌻ id-⧈ {X} ⊞₁ swap-⧈ Y Z
≈-⧈ (associator⇐ ⌻ swap-⧈ (X ⊞ Y) Z) ⌻ associator⇐
hex₂ = eqᵢ ⌸ hexagon₂
where
eqᵢ : (π₂ ×₁ (swap ∘ π₂) ∘ σ₂₃) ∘ ⟨ π₁ , ((assocˡ ∘ π₂) ∘ ⟨ π₁ , ((swap ∘ π₂) ×₁ π₂ ∘ σ₂₃) ∘ assocʳ ×₁ id ⟩) ∘ (id ×₁ swap) ×₁ id ⟩
≈ (assocˡ ∘ π₂) ∘ ⟨ π₁ , ((swap ∘ π₂) ∘ ⟨ π₁ , (assocˡ ∘ π₂) ∘ swap ×₁ id ⟩) ∘ assocʳ ×₁ id ⟩
eqᵢ = begin
(π₂ ×₁ (swap ∘ π₂) ∘ σ₂₃) ∘ ⟨ π₁ , ((_ ∘ π₂) ∘ ⟨ π₁ , _ ∘ _ ×₁ id ⟩) ∘ _ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pullʳ project₂ ⟩∘⟨refl) ⟩
(π₂ ×₁ _ ∘ σ₂₃) ∘ ⟨ π₁ , (_ ∘ ((swap ∘ π₂) ×₁ π₂ ∘ σ₂₃) ∘ _ ×₁ id) ∘ _ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ ((refl⟩∘⟨ ×₁∘⟨⟩ ⟩∘⟨refl) ⟩∘⟨refl) ⟩
_ ∘ ⟨ π₁ , (_ ∘ ⟨ (swap ∘ π₂) ∘ π₁ ×₁ π₁ , π₂ ∘ π₂ ×₁ π₂ ⟩ ∘ _ ×₁ id) ∘ _ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ ((refl⟩∘⟨ ⟨⟩-cong₂ (extendˡ π₂∘×₁) π₂∘×₁ ⟩∘⟨refl) ⟩∘⟨refl) ⟩
_ ∘ ⟨ π₁ , (_ ∘ ⟨ (swap ∘ π₁) ∘ π₂ , π₂ ∘ π₂ ⟩ ∘ assocʳ ×₁ id) ∘ _ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ ((refl⟩∘⟨ pushˡ (sym ⟨⟩∘)) ⟩∘⟨refl) ⟩
(π₂ ×₁ _ ∘ σ₂₃) ∘ ⟨ π₁ , (_ ∘ ⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂ ∘ assocʳ ×₁ id) ∘ _ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (pushˡ (refl⟩∘⟨ refl⟩∘⟨ π₂∘first)) ⟩
(π₂ ×₁ _ ∘ σ₂₃) ∘ ⟨ π₁ , _ ∘ (⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂) ∘ _ ×₁ id ⟩ ≈⟨ refl⟩∘⟨ ⟨⟩-congˡ (refl⟩∘⟨ pullʳ π₂∘first) ⟩
(π₂ ×₁ (swap ∘ π₂) ∘ σ₂₃) ∘ ⟨ π₁ , _ ∘ ⟨ _ ∘ π₁ , π₂ ⟩ ∘ π₂ ⟩ ≈⟨ ×₁∘⟨⟩ ⟩∘⟨refl ⟩
⟨ π₂ ∘ π₁ ×₁ π₁ , (swap ∘ π₂) ∘ π₂ ×₁ π₂ ⟩ ∘ ⟨ π₁ , _ ∘ ⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂ ⟩ ≈⟨ ⟨⟩-cong₂ π₂∘×₁ (extendˡ π₂∘×₁) ⟩∘⟨refl ⟩
⟨ π₁ ∘ π₂ , (swap ∘ π₂) ∘ π₂ ⟩ ∘ ⟨ π₁ , assocˡ ∘ ⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂ ⟩ ≈⟨ pushˡ (sym ⟨⟩∘) ⟩
⟨ π₁ , swap ∘ π₂ ⟩ ∘ π₂ ∘ ⟨ π₁ , assocˡ ∘ ⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂ ⟩ ≈⟨ refl⟩∘⟨ project₂ ⟩
⟨ π₁ , swap ∘ π₂ ⟩ ∘ assocˡ ∘ ⟨ swap ∘ π₁ , π₂ ⟩ ∘ π₂ ≈⟨ ⟨⟩-congʳ (sym identityˡ) ⟩∘⟨ pushʳ (⟨⟩-congˡ (sym identityˡ) ⟩∘⟨refl) ⟩
id ×₁ swap ∘ (assocˡ ∘ swap ×₁ id) ∘ π₂ ≈⟨ extendʳ (hexagon₂-inv braided) ⟩
assocˡ ∘ (swap ∘ assocˡ) ∘ π₂ ≈⟨ refl⟩∘⟨ pullʳ (pushʳ (sym π₂∘first)) ⟩
assocˡ ∘ swap ∘ (assocˡ ∘ π₂) ∘ assocʳ ×₁ id ≈⟨ refl⟩∘⟨ refl⟩∘⟨ pushʳ (sym π₂∘first) ⟩∘⟨refl ⟩
assocˡ ∘ swap ∘ ((assocˡ ∘ π₂) ∘ swap ×₁ id) ∘ assocʳ ×₁ id ≈⟨ refl⟩∘⟨ pullˡ (pushʳ (sym project₂)) ⟩
assocˡ ∘ ((swap ∘ π₂) ∘ ⟨ π₁ , (assocˡ ∘ π₂) ∘ swap ×₁ id ⟩) ∘ assocʳ ×₁ id ≈⟨ pushʳ (sym project₂) ⟩
(assocˡ ∘ π₂) ∘ ⟨ π₁ , ((_ ∘ π₂) ∘ ⟨ π₁ , (_ ∘ π₂) ∘ swap ×₁ id ⟩) ∘ _ ×₁ id ⟩ ∎
module Directed where
open D using (-⊞-)
γ : -⊞- ≃ flip-bifunctor -⊞-
γ = niHelper record
{ η = uncurry swap-⧈
; η⁻¹ = uncurry (flip swap-⧈)
; commute = uncurry swap-commute
; iso = λ (X , Y) → record
{ isoˡ = swap∘swap-⧈
; isoʳ = swap∘swap-⧈
}
}
module Balanced where
open B using (-⊞-)
γ : -⊞- ≃ flip-bifunctor -⊞-
γ = niHelper record
{ η = λ (X , Y) → swap-⧈ (X □ X) (Y □ Y)
; η⁻¹ = λ (X , Y) → swap-⧈ (Y □ Y) (X □ X)
; commute = uncurry swap-commute
; iso = λ (X , Y) → record
{ isoˡ = swap∘swap-⧈
; isoʳ = swap∘swap-⧈
}
}
DWD-Braided : Braided DWD-Monoidal
DWD-Braided = record
{ braiding = Directed.γ
; hexagon₁ = hex₁
; hexagon₂ = hex₂
}
BWD-Braided : Braided BWD-Monoidal
BWD-Braided = record
{ braiding = Balanced.γ
; hexagon₁ = hex₁
; hexagon₂ = hex₂
}
|
