Skip to content

Commit ee8238f

Browse files
tillrampetillrampe
committed
Improve indentation
1 parent 0d545ff commit ee8238f

File tree

1 file changed

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

1 file changed

+36
-36
lines changed

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

Lines changed: 36 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -56,51 +56,54 @@ open Left-Unitor using (unitorˡ-⊗-from) renaming (triangle to unitorˡ-triang
5656
open Right-Unitor using (unitorʳ-⊗-from) renaming (triangle to unitorʳ-triangle)
5757

5858
abstract
59-
triangle-⊗-∘arr² : ((α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
60-
∘ᵥ α (associator-⊗-from {B₃ = B₂} {Id-Bimod} {B₁}))
61-
∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
62-
∘ᵥ arr (CoeqBimods B₂ Id-Bimod) ◁ F B₁
63-
≈ (α (unitorʳ-⊗-from {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
64-
∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
65-
∘ᵥ arr (CoeqBimods B₂ Id-Bimod) ◁ F B₁
59+
triangle-⊗-∘arr² :
60+
((α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
61+
∘ᵥ α (associator-⊗-from {B₃ = B₂} {Id-Bimod} {B₁}))
62+
∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
63+
∘ᵥ arr (CoeqBimods B₂ Id-Bimod) ◁ F B₁
64+
≈
65+
(α (unitorʳ-⊗-from {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
66+
∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
67+
∘ᵥ arr (CoeqBimods B₂ Id-Bimod) ◁ F B₁
68+
6669
triangle-⊗-∘arr² = begin
6770

6871
((α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
6972
∘ᵥ α (associator-⊗-from {B₃ = B₂} {Id-Bimod} {B₁}))
7073
∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
7174
∘ᵥ arr (CoeqBimods B₂ Id-Bimod) ◁ F B₁
72-
≈⟨ assoc₂ ⟩
75+
≈⟨ assoc₂ ⟩
7376

7477
(α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
7578
∘ᵥ α (associator-⊗-from {B₃ = B₂} {Id-Bimod} {B₁}))
7679
∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁)
7780
∘ᵥ arr (CoeqBimods B₂ Id-Bimod) ◁ F B₁
78-
≈⟨ extendˡ (⟺ (hexagon-sq {B₃ = B₂} {Id-Bimod} {B₁})) ⟩
81+
≈⟨ extendˡ (⟺ (hexagon-sq {B₃ = B₂} {Id-Bimod} {B₁})) ⟩
7982

8083
(α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
8184
∘ᵥ (arr (CoeqBimods B₂ (Id-Bimod ⊗₀ B₁))
8285
∘ᵥ F B₂ ▷ arr (CoeqBimods Id-Bimod B₁)))
8386
∘ᵥ α⇒ {f = F B₂} {T M₂} {F B₁}
84-
≈⟨ ⟺ (pullˡ associator-∘⇒unitor-⊗) ⟩
87+
≈⟨ ⟺ (pullˡ associator-∘⇒unitor-⊗) ⟩
8588

8689
(arr (CoeqBimods B₂ B₁)
8790
∘ᵥ actionˡ B₂ ◁ F B₁)
8891
∘ᵥ α⇐ {f = F B₂} {T M₂} {F B₁}
8992
∘ᵥ α⇒ {f = F B₂} {T M₂} {F B₁}
90-
≈⟨ elimʳ associator.isoˡ ⟩
93+
≈⟨ elimʳ associator.isoˡ ⟩
9194

9295
arr (CoeqBimods B₂ B₁)
9396
∘ᵥ actionˡ B₂ ◁ F B₁
94-
≈⟨ id⇒unitor-⊗ ⟩
97+
≈⟨ id⇒unitor-⊗ ⟩
9598

9699
α (unitorʳ-⊗-from {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
97100
∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁)
98101
∘ᵥ arr (CoeqBimods B₂ Id-Bimod) ◁ F B₁
99-
≈⟨ ⟺ assoc₂ ⟩
102+
≈⟨ ⟺ assoc₂ ⟩
100103

101104
(α (unitorʳ-⊗-from {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
102105
∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
103-
∘ᵥ arr (CoeqBimods B₂ Id-Bimod) ◁ F B₁ ∎
106+
∘ᵥ arr (CoeqBimods B₂ Id-Bimod) ◁ F B₁ ∎
104107

105108
where
106109
open hom.HomReasoning
@@ -124,8 +127,7 @@ abstract
124127
∘ᵥ α⇐ {f = F B₂} {T M₂} {F B₁} ≈⟨ ⟺ (equality (CoeqBimods B₂ B₁)) ⟩
125128

126129
arr (CoeqBimods B₂ B₁)
127-
∘ᵥ F B₂ ▷ actionʳ B₁ ≈⟨ ⟺ (glue▹◽ (▷-resp-tri unitorˡ-triangle) (⟺ (αSq-⊗ id-bimodule-hom unitorˡ-⊗-from)))
128-
⟩
130+
∘ᵥ F B₂ ▷ actionʳ B₁ ≈⟨ ⟺ (glue▹◽ (▷-resp-tri unitorˡ-triangle) (⟺ (αSq-⊗ id-bimodule-hom unitorˡ-⊗-from))) ⟩
129131

130132
α (id-bimodule-hom ⊗₁ unitorˡ-⊗-from)
131133
∘ᵥ arr (CoeqBimods B₂ (Id-Bimod ⊗₀ B₁))
@@ -141,28 +143,26 @@ abstract
141143

142144
id⇒unitor-⊗ = ⟺ (glue▹◽ (◁-resp-tri unitorʳ-triangle) (⟺ (αSq-⊗ unitorʳ-⊗-from id-bimodule-hom)))
143145

144-
triangle-⊗-∘arr : (α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
145-
∘ᵥ α (associator-⊗-from {B₃ = B₂} {Id-Bimod} {B₁}))
146-
∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁)
147-
≈ α (unitorʳ-⊗-from {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
148-
∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁)
146+
147+
triangle-⊗-∘arr :
148+
(α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
149+
∘ᵥ α (associator-⊗-from {B₃ = B₂} {Id-Bimod} {B₁}))
150+
∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁)
151+
≈
152+
α (unitorʳ-⊗-from {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
153+
∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁)
149154

150155
triangle-⊗-∘arr = Coequalizer⇒Epi
151-
((CoeqBimods B₂ Id-Bimod) coeq-◁ F B₁)
152-
((α (id-bimodule-hom ⊗₁ unitorˡ-⊗-from)
153-
∘ᵥ α associator-⊗-from)
154-
∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
155-
(α (unitorʳ-⊗-from ⊗₁ id-bimodule-hom)
156-
∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
157-
triangle-⊗-∘arr²
156+
((CoeqBimods B₂ Id-Bimod) coeq-◁ F B₁)
157+
((α (id-bimodule-hom ⊗₁ unitorˡ-⊗-from) ∘ᵥ α associator-⊗-from) ∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
158+
(α (unitorʳ-⊗-from ⊗₁ id-bimodule-hom) ∘ᵥ arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
159+
triangle-⊗-∘arr²
158160

159-
triangle-⊗ : α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
160-
∘ᵥ α (associator-⊗-from {B₃ = B₂} {Id-Bimod} {B₁})
161-
≈ α (unitorʳ-⊗-from {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
161+
triangle-⊗ : α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁}) ∘ᵥ α (associator-⊗-from {B₃ = B₂} {Id-Bimod} {B₁})
162+
≈ α (unitorʳ-⊗-from {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
162163

163164
triangle-⊗ = Coequalizer⇒Epi
164-
(CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁)
165-
(α (id-bimodule-hom ⊗₁ unitorˡ-⊗-from)
166-
∘ᵥ α associator-⊗-from)
167-
(α (unitorʳ-⊗-from ⊗₁ id-bimodule-hom))
168-
triangle-⊗-∘arr
165+
(CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁)
166+
(α (id-bimodule-hom ⊗₁ unitorˡ-⊗-from) ∘ᵥ α associator-⊗-from)
167+
(α (unitorʳ-⊗-from ⊗₁ id-bimodule-hom))
168+
triangle-⊗-∘arr

0 commit comments

Comments
 (0)