Skip to content

Commit e4f1326

Browse files
tillrampetillrampe
committed
Improve indentation
1 parent cc45b69 commit e4f1326

File tree

1 file changed

+18
-20
lines changed
  • src/Categories/Bicategory/Construction/Bimodules/Tensorproduct/Coherence

1 file changed

+18
-20
lines changed

‎src/Categories/Bicategory/Construction/Bimodules/Tensorproduct/Coherence/Pentagon.agda‎

Lines changed: 18 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -86,24 +86,25 @@ abstract
8686
(α⇒ {f = F B₄} {F B₃} {F B₂ ∘₁ F B₁})
8787
(α (associator-⊗-from {B₃ = B₄} {B₃} {B₂ ⊗₀ B₁}))
8888
((arr (CoeqBimods B₄ (B₃ ⊗₀ B₂ ⊗₀ B₁)) ∘ᵥ F B₄ ▷ arr (CoeqBimods B₃ (B₂ ⊗₀ B₁))) ∘ᵥ F B₄ ▷ F B₃ ▷ arr (CoeqBimods B₂ B₁))
89+
8990
face[43]21⇒4321 = begin
9091

9192
α (associator-⊗-from {B₃ = B₄} {B₃} {B₂ ⊗₀ B₁})
9293
∘ᵥ (arr (CoeqBimods (B₄ ⊗₀ B₃) (B₂ ⊗₀ B₁))
9394
∘ᵥ F (B₄ ⊗₀ B₃) ▷ arr (CoeqBimods B₂ B₁))
9495
∘ᵥ arr (CoeqBimods B₄ B₃) ◁ (F B₂ ∘₁ F B₁)
95-
≈⟨ refl⟩∘⟨ extendˡ ◁-▷-exchg ⟩
96+
≈⟨ refl⟩∘⟨ extendˡ ◁-▷-exchg ⟩
9697

9798
α (associator-⊗-from {B₃ = B₄} {B₃} {B₂ ⊗₀ B₁})
9899
∘ᵥ (arr (CoeqBimods (B₄ ⊗₀ B₃) (B₂ ⊗₀ B₁))
99100
∘ᵥ arr (CoeqBimods B₄ B₃) ◁ F (B₂ ⊗₀ B₁))
100101
∘ᵥ (F B₄ ∘₁ F B₃) ▷ arr (CoeqBimods B₂ B₁)
101-
≈⟨ glue′ (⟺ (hexagon-sq {B₃ = B₄} {B₃} {B₂ ⊗₀ B₁})) α⇒-▷-∘₁ ⟩
102+
≈⟨ glue′ (⟺ (hexagon-sq {B₃ = B₄} {B₃} {B₂ ⊗₀ B₁})) α⇒-▷-∘₁ ⟩
102103

103104
((arr (CoeqBimods B₄ (B₃ ⊗₀ B₂ ⊗₀ B₁))
104105
∘ᵥ F B₄ ▷ arr (CoeqBimods B₃ (B₂ ⊗₀ B₁)))
105106
∘ᵥ F B₄ ▷ F B₃ ▷ arr (CoeqBimods B₂ B₁))
106-
∘ᵥ α⇒ {f = F B₄} {F B₃} {F B₂ ∘₁ F B₁} ∎
107+
∘ᵥ α⇒ {f = F B₄} {F B₃} {F B₂ ∘₁ F B₁} ∎
107108

108109
where
109110
open hom.HomReasoning
@@ -120,22 +121,22 @@ abstract
120121
α (associator-⊗-from {B₃ = B₄} {B₃} {B₂} ◁-⊗ B₁)
121122
∘ᵥ (arr (CoeqBimods ((B₄ ⊗₀ B₃) ⊗₀ B₂) B₁)
122123
∘ᵥ arr (CoeqBimods (B₄ ⊗₀ B₃) B₂) ◁ F B₁)
123-
∘ᵥ arr (CoeqBimods B₄ B₃) ◁ F B₂ ◁ F B₁ ≈⟨ refl⟩∘⟨ assoc₂ ⟩
124+
∘ᵥ arr (CoeqBimods B₄ B₃) ◁ F B₂ ◁ F B₁ ≈⟨ refl⟩∘⟨ assoc₂ ⟩
124125

125126
α (associator-⊗-from {B₃ = B₄} {B₃} {B₂} ◁-⊗ B₁)
126127
∘ᵥ arr (CoeqBimods ((B₄ ⊗₀ B₃) ⊗₀ B₂) B₁)
127128
∘ᵥ arr (CoeqBimods (B₄ ⊗₀ B₃) B₂) ◁ F B₁
128-
∘ᵥ arr (CoeqBimods B₄ B₃) ◁ F B₂ ◁ F B₁ ≈⟨ ⟺ (glue αSq-⊗ (◁-resp-long-sq′ hexagon-sq)) ⟩
129+
∘ᵥ arr (CoeqBimods B₄ B₃) ◁ F B₂ ◁ F B₁ ≈⟨ ⟺ (glue αSq-⊗ (◁-resp-long-sq′ hexagon-sq)) ⟩
129130

130131
(arr (CoeqBimods (B₄ ⊗₀ B₃ ⊗₀ B₂) B₁)
131132
∘ᵥ arr (CoeqBimods B₄ (B₃ ⊗₀ B₂)) ◁ F B₁
132133
∘ᵥ (F B₄ ▷ arr (CoeqBimods B₃ B₂)) ◁ F B₁)
133-
∘ᵥ α⇒ {f = F B₄} {F B₃} {F B₂} ◁ F B₁ ≈⟨ ⟺ assoc₂ ⟩∘⟨refl ⟩
134+
∘ᵥ α⇒ {f = F B₄} {F B₃} {F B₂} ◁ F B₁ ≈⟨ ⟺ assoc₂ ⟩∘⟨refl ⟩
134135

135136
((arr (CoeqBimods (B₄ ⊗₀ B₃ ⊗₀ B₂) B₁)
136137
∘ᵥ arr (CoeqBimods B₄ (B₃ ⊗₀ B₂)) ◁ F B₁)
137138
∘ᵥ (F B₄ ▷ arr (CoeqBimods B₃ B₂)) ◁ F B₁)
138-
∘ᵥ α⇒ {f = F B₄} {F B₃} {F B₂} ◁ F B₁ ∎
139+
∘ᵥ α⇒ {f = F B₄} {F B₃} {F B₂} ◁ F B₁ ∎
139140

140141
where
141142
open hom.HomReasoning
@@ -165,25 +166,22 @@ abstract
165166
α (B₄ ⊗-▷ associator-⊗-from {B₃ = B₃} {B₂} {B₁})
166167
∘ᵥ (arr (CoeqBimods B₄ ((B₃ ⊗₀ B₂) ⊗₀ B₁))
167168
∘ᵥ F B₄ ▷ arr (CoeqBimods (B₃ ⊗₀ B₂) B₁))
168-
∘ᵥ F B₄ ▷ (arr (CoeqBimods B₃ B₂) ◁ F B₁) ≈⟨ refl⟩∘⟨ assoc₂ ⟩
169+
∘ᵥ F B₄ ▷ (arr (CoeqBimods B₃ B₂) ◁ F B₁) ≈⟨ refl⟩∘⟨ assoc₂ ⟩
169170

170171
α (B₄ ⊗-▷ associator-⊗-from {B₃ = B₃} {B₂} {B₁})
171172
∘ᵥ arr (CoeqBimods B₄ ((B₃ ⊗₀ B₂) ⊗₀ B₁))
172173
∘ᵥ F B₄ ▷ arr (CoeqBimods (B₃ ⊗₀ B₂) B₁)
173-
∘ᵥ F B₄ ▷ (arr (CoeqBimods B₃ B₂) ◁ F B₁) ≈⟨ glue′
174-
(⟺ αSq-⊗)
175-
(▷-resp-long-sq (⟺ (hexagon-sq {B₃ = B₃} {B₂} {B₁})))
176-
⟩
174+
∘ᵥ F B₄ ▷ (arr (CoeqBimods B₃ B₂) ◁ F B₁) ≈⟨ glue′ (⟺ αSq-⊗) (▷-resp-long-sq (⟺ (hexagon-sq {B₃ = B₃} {B₂} {B₁}))) ⟩
177175

178176
(arr (CoeqBimods B₄ (B₃ ⊗₀ B₂ ⊗₀ B₁))
179177
∘ᵥ F B₄ ▷ arr (CoeqBimods B₃ (B₂ ⊗₀ B₁))
180178
∘ᵥ F B₄ ▷ F B₃ ▷ arr (CoeqBimods B₂ B₁))
181-
∘ᵥ F B₄ ▷ α⇒ {f = F B₃} {F B₂} {F B₁} ≈⟨ ⟺ assoc₂ ⟩∘⟨refl ⟩
179+
∘ᵥ F B₄ ▷ α⇒ {f = F B₃} {F B₂} {F B₁} ≈⟨ ⟺ assoc₂ ⟩∘⟨refl ⟩
182180

183181
((arr (CoeqBimods B₄ (B₃ ⊗₀ B₂ ⊗₀ B₁))
184182
∘ᵥ F B₄ ▷ arr (CoeqBimods B₃ (B₂ ⊗₀ B₁)))
185183
∘ᵥ F B₄ ▷ F B₃ ▷ arr (CoeqBimods B₂ B₁))
186-
∘ᵥ F B₄ ▷ α⇒ {f = F B₃} {F B₂} {F B₁} ∎
184+
∘ᵥ F B₄ ▷ α⇒ {f = F B₃} {F B₂} {F B₁} ∎
187185

188186
where
189187
open hom.HomReasoning
@@ -213,43 +211,43 @@ abstract
213211
∘ᵥ arr (CoeqBimods ((B₄ ⊗₀ B₃) ⊗₀ B₂) B₁))
214212
∘ᵥ arr (CoeqBimods (B₄ ⊗₀ B₃) B₂) ◁ F B₁)
215213
∘ᵥ arr (CoeqBimods B₄ B₃) ◁ F B₂ ◁ F B₁
216-
≈⟨ assoc²αδ ⟩
214+
≈⟨ assoc²αδ ⟩
217215

218216
(α (B₄ ⊗-▷ associator-⊗-from {B₃ = B₃} {B₂} {B₁})
219217
∘ᵥ α (associator-⊗-from {B₃ = B₄} {B₃ ⊗₀ B₂} {B₁})
220218
∘ᵥ α (associator-⊗-from {B₃ = B₄} {B₃} {B₂} ◁-⊗ B₁))
221219
∘ᵥ (arr (CoeqBimods ((B₄ ⊗₀ B₃) ⊗₀ B₂) B₁)
222220
∘ᵥ arr (CoeqBimods (B₄ ⊗₀ B₃) B₂) ◁ F B₁)
223221
∘ᵥ arr (CoeqBimods B₄ B₃) ◁ F B₂ ◁ F B₁
224-
≈⟨ glue face4[32]1⇒4321 (glue face[432]1⇒4[32]1 face[[43]2]1⇒[432]1) ⟩
222+
≈⟨ glue face4[32]1⇒4321 (glue face[432]1⇒4[32]1 face[[43]2]1⇒[432]1) ⟩
225223

226224
((arr (CoeqBimods B₄ (B₃ ⊗₀ B₂ ⊗₀ B₁))
227225
∘ᵥ F B₄ ▷ arr (CoeqBimods B₃ (B₂ ⊗₀ B₁)))
228226
∘ᵥ F B₄ ▷ F B₃ ▷ arr (CoeqBimods B₂ B₁))
229227
∘ᵥ F B₄ ▷ α⇒ {f = F B₃} {F B₂} {F B₁}
230228
∘ᵥ α⇒ {f = F B₄} {F B₃ ∘₁ F B₂} {F B₁}
231229
∘ᵥ α⇒ {f = F B₄} {F B₃} {F B₂} ◁ F B₁
232-
≈⟨ refl⟩∘⟨ pentagon ⟩
230+
≈⟨ refl⟩∘⟨ pentagon ⟩
233231

234232
((arr (CoeqBimods B₄ (B₃ ⊗₀ B₂ ⊗₀ B₁))
235233
∘ᵥ F B₄ ▷ arr (CoeqBimods B₃ (B₂ ⊗₀ B₁)))
236234
∘ᵥ F B₄ ▷ F B₃ ▷ arr (CoeqBimods B₂ B₁))
237235
∘ᵥ α⇒ {f = F B₄} {F B₃} {F B₂ ∘₁ F B₁}
238236
∘ᵥ α⇒ {f = F B₄ ∘₁ F B₃} {F B₂} {F B₁}
239-
≈⟨ ⟺ (glue face[43]21⇒4321 face[[43]2]1⇒[43]21) ⟩
237+
≈⟨ ⟺ (glue face[43]21⇒4321 face[[43]2]1⇒[43]21) ⟩
240238

241239
(α (associator-⊗-from {B₃ = B₄} {B₃} {B₂ ⊗₀ B₁})
242240
∘ᵥ α (associator-⊗-from {B₃ = B₄ ⊗₀ B₃} {B₂} {B₁}))
243241
∘ᵥ (arr (CoeqBimods ((B₄ ⊗₀ B₃) ⊗₀ B₂) B₁)
244242
∘ᵥ arr (CoeqBimods (B₄ ⊗₀ B₃) B₂) ◁ F B₁)
245243
∘ᵥ arr (CoeqBimods B₄ B₃) ◁ F B₂ ◁ F B₁
246-
≈⟨ assoc²δα ⟩
244+
≈⟨ assoc²δα ⟩
247245

248246
(((α (associator-⊗-from {B₃ = B₄} {B₃} {B₂ ⊗₀ B₁})
249247
∘ᵥ α (associator-⊗-from {B₃ = B₄ ⊗₀ B₃} {B₂} {B₁}))
250248
∘ᵥ arr (CoeqBimods ((B₄ ⊗₀ B₃) ⊗₀ B₂) B₁))
251249
∘ᵥ arr (CoeqBimods (B₄ ⊗₀ B₃) B₂) ◁ F B₁)
252-
∘ᵥ arr (CoeqBimods B₄ B₃) ◁ F B₂ ◁ F B₁ ∎
250+
∘ᵥ arr (CoeqBimods B₄ B₃) ◁ F B₂ ◁ F B₁ ∎
253251

254252
where
255253
open hom.HomReasoning

0 commit comments

Comments
 (0)