Adapt to the name changes in Unitor.agda

Author: tillrampe

src/Categories/Bicategory/Construction/Bimodules.agda

@@ -46,16 +46,16 @@ Bimodules = record
       ; iso = λ ((B₃ , B₂) , B₁) → _≅_.iso (associator-⊗ {B₃ = B₃} {B₂} {B₁})
       }
     ; unitˡ = niHelper record
-      { η = λ (_ , B) → _≅_.from (Unitorˡ⊗ {B = B})
-      ; η⁻¹ = λ (_ , B) → _≅_.to (Unitorˡ⊗ {B = B})
-      ; commute = λ (_ , f) → λ⇒⊗-natural f
-      ; iso = λ (_ , B) → _≅_.iso (Unitorˡ⊗ {B = B})
+      { η = λ (_ , B) → _≅_.from (unitorˡ-⊗ {B = B})
+      ; η⁻¹ = λ (_ , B) → _≅_.to (unitorˡ-⊗ {B = B})
+      ; commute = λ (_ , f) → λ⇒-⊗-natural f
+      ; iso = λ (_ , B) → _≅_.iso (unitorˡ-⊗ {B = B})
       }
     ; unitʳ = niHelper record
-      { η = λ (B , _) → _≅_.from (Unitorʳ⊗ {B = B})
-      ; η⁻¹ = λ (B , _) → _≅_.to (Unitorʳ⊗ {B = B})
-      ; commute = λ (f , _) → ρ⇒⊗-natural f
-      ; iso = λ (B , _) → _≅_.iso (Unitorʳ⊗ {B = B})
+      { η = λ (B , _) → _≅_.from (unitorʳ-⊗ {B = B})
+      ; η⁻¹ = λ (B , _) → _≅_.to (unitorʳ-⊗ {B = B})
+      ; commute = λ (f , _) → ρ⇒-⊗-natural f
+      ; iso = λ (B , _) → _≅_.iso (unitorʳ-⊗ {B = B})
       }
     }
   ; triangle = λ {_} {_} {_} {B₁} {B₂} → triangle⊗ {B₂ = B₂} {B₁}
@@ -73,11 +73,11 @@ Bimodules = record
     open import Categories.Bicategory.Construction.Bimodules.Tensorproduct.Associator.Naturality {𝒞 = 𝒞} {localCoeq}
       using (α⇒-⊗-natural)
     import Categories.Bicategory.Construction.Bimodules.Tensorproduct.Unitor {𝒞 = 𝒞} {localCoeq} as Unitor
-    open Unitor.Left-Unitor using (Unitorˡ⊗)
-    open Unitor.Right-Unitor using (Unitorʳ⊗)
+    open Unitor.Left-Unitor using (unitorˡ-⊗)
+    open Unitor.Right-Unitor using (unitorʳ-⊗)
     import Categories.Bicategory.Construction.Bimodules.Tensorproduct.Unitor.Naturality {𝒞 = 𝒞} {localCoeq} as Unitor-Naturality
-    open Unitor-Naturality.Left-Unitor-natural using (λ⇒⊗-natural)
-    open Unitor-Naturality.Right-Unitor-natural using (ρ⇒⊗-natural)
+    open Unitor-Naturality.Left-Unitor-natural using (λ⇒-⊗-natural)
+    open Unitor-Naturality.Right-Unitor-natural using (ρ⇒-⊗-natural)
     open import Categories.Bicategory.Construction.Bimodules.Tensorproduct.Coherence.Pentagon {𝒞 = 𝒞} {localCoeq}
       using (pentagon⊗)
     open import Categories.Bicategory.Construction.Bimodules.Tensorproduct.Coherence.Triangle {𝒞 = 𝒞} {localCoeq}

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

@@ -47,8 +47,8 @@ open import Categories.Bicategory.Construction.Bimodules.Tensorproduct.Associato
   using (associator-⊗-from; hexagon)
 import Categories.Bicategory.Construction.Bimodules.Tensorproduct.Unitor
   {𝒞 = 𝒞} {localCoeq} as Unitor
-open Unitor.Left-Unitor using (Unitorˡ⊗From) renaming (triangle to left-unitor-triangle)
-open Unitor.Right-Unitor using (Unitorʳ⊗From) renaming (triangle to right-unitor-triangle)
+open Unitor.Left-Unitor using (unitorˡ-⊗-from) renaming (triangle to left-unitor-triangle)
+open Unitor.Right-Unitor using (unitorʳ-⊗-from) renaming (triangle to right-unitor-triangle)
 
 open TensorproductOfBimodules using (CoeqBimods)
 open TensorproductOfHomomorphisms using (αSq-⊗)
@@ -58,65 +58,65 @@ open Bimodule B₁ using () renaming (F to F₁; actionʳ to actionʳ₁)
 open Bimodule B₂ using () renaming (F to F₂; actionˡ to actionˡ₂)
 
 abstract
-  triangle⊗∘arr² : ((Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ Unitorˡ⊗From {B = B₁})
+  triangle⊗∘arr² : ((Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
                    ∘ᵥ Bimodhom.α (associator-⊗-from {B₃ = B₂} {Id-Bimod} {B₁}))
                    ∘ᵥ Coequalizer.arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
                    ∘ᵥ Coequalizer.arr (CoeqBimods B₂ Id-Bimod) ◁ F₁
-                   ≈ (Bimodhom.α (Unitorʳ⊗From {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
+                   ≈ (Bimodhom.α (unitorʳ-⊗-from {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
                      ∘ᵥ Coequalizer.arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
                      ∘ᵥ Coequalizer.arr (CoeqBimods B₂ Id-Bimod) ◁ F₁
   triangle⊗∘arr² = begin
 
-    ((Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ Unitorˡ⊗From {B = B₁})
+    ((Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
     ∘ᵥ Bimodhom.α (associator-⊗-from {B₃ = B₂} {Id-Bimod} {B₁}))
     ∘ᵥ Coequalizer.arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
     ∘ᵥ Coequalizer.arr (CoeqBimods B₂ Id-Bimod) ◁ F₁
     ≈⟨ assoc₂ ⟩
 
-    (Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ Unitorˡ⊗From {B = B₁})
+    (Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
     ∘ᵥ Bimodhom.α (associator-⊗-from {B₃ = B₂} {Id-Bimod} {B₁}))
     ∘ᵥ Coequalizer.arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁)
     ∘ᵥ Coequalizer.arr (CoeqBimods B₂ Id-Bimod) ◁ F₁
     ≈⟨ assoc₂ ⟩
 
-    Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ Unitorˡ⊗From {B = B₁})
+    Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
     ∘ᵥ Bimodhom.α (associator-⊗-from {B₃ = B₂} {Id-Bimod} {B₁})
     ∘ᵥ Coequalizer.arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁)
     ∘ᵥ Coequalizer.arr (CoeqBimods B₂ Id-Bimod) ◁ F₁
     ≈⟨ refl⟩∘⟨ ⟺ (hexagon {B₃ = B₂} {Id-Bimod} {B₁}) ⟩
 
-    Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ Unitorˡ⊗From {B = B₁})
+    Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
     ∘ᵥ Coequalizer.arr (CoeqBimods B₂ (Id-Bimod ⊗₀ B₁))
     ∘ᵥ F₂ ▷ Coequalizer.arr (CoeqBimods Id-Bimod B₁)
     ∘ᵥ associator.from {f = F₂} {T₂} {F₁}
     ≈⟨ sym-assoc₂ ⟩
 
-    (Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ Unitorˡ⊗From {B = B₁})
+    (Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
     ∘ᵥ Coequalizer.arr (CoeqBimods B₂ (Id-Bimod ⊗₀ B₁)))
     ∘ᵥ F₂ ▷ Coequalizer.arr (CoeqBimods Id-Bimod B₁)
     ∘ᵥ associator.from {f = F₂} {T₂} {F₁}
-    ≈⟨ ⟺ (αSq-⊗ (id-bimodule-hom {B = B₂}) (Unitorˡ⊗From {B = B₁})) ⟩∘⟨refl ⟩
+    ≈⟨ ⟺ (αSq-⊗ (id-bimodule-hom {B = B₂}) (unitorˡ-⊗-from {B = B₁})) ⟩∘⟨refl ⟩
 
     (Coequalizer.arr (CoeqBimods B₂ B₁)
-    ∘ᵥ F₂ ▷ Bimodhom.α (Unitorˡ⊗From {B = B₁}))
+    ∘ᵥ F₂ ▷ Bimodhom.α (unitorˡ-⊗-from {B = B₁}))
     ∘ᵥ F₂ ▷ Coequalizer.arr (CoeqBimods Id-Bimod B₁)
     ∘ᵥ associator.from {f = F₂} {T₂} {F₁}
     ≈⟨ assoc₂ ⟩
 
     Coequalizer.arr (CoeqBimods B₂ B₁)
-    ∘ᵥ F₂ ▷ Bimodhom.α (Unitorˡ⊗From {B = B₁})
+    ∘ᵥ F₂ ▷ Bimodhom.α (unitorˡ-⊗-from {B = B₁})
     ∘ᵥ F₂ ▷ Coequalizer.arr (CoeqBimods Id-Bimod B₁)
     ∘ᵥ associator.from {f = F₂} {T₂} {F₁}
     ≈⟨ refl⟩∘⟨ sym-assoc₂ ⟩
 
     Coequalizer.arr (CoeqBimods B₂ B₁)
-    ∘ᵥ (F₂ ▷ Bimodhom.α (Unitorˡ⊗From {B = B₁})
+    ∘ᵥ (F₂ ▷ Bimodhom.α (unitorˡ-⊗-from {B = B₁})
     ∘ᵥ F₂ ▷ Coequalizer.arr (CoeqBimods Id-Bimod B₁))
     ∘ᵥ associator.from {f = F₂} {T₂} {F₁}
     ≈⟨ refl⟩∘⟨ ∘ᵥ-distr-▷ ⟩∘⟨refl ⟩
 
     Coequalizer.arr (CoeqBimods B₂ B₁)
-    ∘ᵥ F₂ ▷ (Bimodhom.α (Unitorˡ⊗From {B = B₁})
+    ∘ᵥ F₂ ▷ (Bimodhom.α (unitorˡ-⊗-from {B = B₁})
             ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B₁))
     ∘ᵥ associator.from {f = F₂} {T₂} {F₁}
     ≈⟨ refl⟩∘⟨ ▷-resp-≈ (left-unitor-triangle {B = B₁}) ⟩∘⟨refl ⟩
@@ -136,21 +136,21 @@ abstract
     ≈⟨ refl⟩∘⟨ ◁-resp-≈ ( ⟺ (right-unitor-triangle {B = B₂})) ⟩
 
     Coequalizer.arr (CoeqBimods B₂ B₁)
-    ∘ᵥ (Bimodhom.α (Unitorʳ⊗From {B = B₂})
+    ∘ᵥ (Bimodhom.α (unitorʳ-⊗-from {B = B₂})
         ∘ᵥ Coequalizer.arr (CoeqBimods B₂ Id-Bimod)) ◁ F₁
     ≈⟨ refl⟩∘⟨ ⟺ ∘ᵥ-distr-◁ ⟩
 
     Coequalizer.arr (CoeqBimods B₂ B₁)
-    ∘ᵥ Bimodhom.α (Unitorʳ⊗From {B = B₂}) ◁ F₁
+    ∘ᵥ Bimodhom.α (unitorʳ-⊗-from {B = B₂}) ◁ F₁
     ∘ᵥ Coequalizer.arr (CoeqBimods B₂ Id-Bimod) ◁ F₁
     ≈⟨ sym-assoc₂ ⟩
 
     (Coequalizer.arr (CoeqBimods B₂ B₁)
-    ∘ᵥ Bimodhom.α (Unitorʳ⊗From {B = B₂}) ◁ F₁)
+    ∘ᵥ Bimodhom.α (unitorʳ-⊗-from {B = B₂}) ◁ F₁)
     ∘ᵥ Coequalizer.arr (CoeqBimods B₂ Id-Bimod) ◁ F₁
-    ≈⟨ αSq-⊗ (Unitorʳ⊗From {B = B₂}) (id-bimodule-hom {B = B₁}) ⟩∘⟨refl ⟩
+    ≈⟨ αSq-⊗ (unitorʳ-⊗-from {B = B₂}) (id-bimodule-hom {B = B₁}) ⟩∘⟨refl ⟩
 
-    (Bimodhom.α (Unitorʳ⊗From {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
+    (Bimodhom.α (unitorʳ-⊗-from {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
     ∘ᵥ Coequalizer.arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
     ∘ᵥ Coequalizer.arr (CoeqBimods B₂ Id-Bimod) ◁ F₁ ∎
 
@@ -167,28 +167,28 @@ abstract
         Coequalizer.arr (CoeqBimods B₂ B₁) ∘ᵥ actionˡ₂ ◁ F₁ ∘ᵥ associator.to ≈⟨ ⟺ (Coequalizer.equality (CoeqBimods B₂ B₁)) ⟩
         Coequalizer.arr (CoeqBimods B₂ B₁) ∘ᵥ F₂ ▷ actionʳ₁ ∎
 
-  triangle⊗∘arr : (Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ Unitorˡ⊗From {B = B₁})
+  triangle⊗∘arr : (Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
                   ∘ᵥ Bimodhom.α (associator-⊗-from {B₃ = B₂} {Id-Bimod} {B₁}))
                   ∘ᵥ Coequalizer.arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁)
-                  ≈ Bimodhom.α (Unitorʳ⊗From {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
+                  ≈ Bimodhom.α (unitorʳ-⊗-from {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
                     ∘ᵥ Coequalizer.arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁)
 
   triangle⊗∘arr = Coequalizer⇒Epi
                     ((CoeqBimods B₂ Id-Bimod) coeq-◁ F₁)
-                    ((Bimodhom.α (id-bimodule-hom ⊗₁ Unitorˡ⊗From)
+                    ((Bimodhom.α (id-bimodule-hom ⊗₁ unitorˡ-⊗-from)
                     ∘ᵥ Bimodhom.α associator-⊗-from)
                     ∘ᵥ Coequalizer.arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
-                    (Bimodhom.α (Unitorʳ⊗From ⊗₁ id-bimodule-hom)
+                    (Bimodhom.α (unitorʳ-⊗-from ⊗₁ id-bimodule-hom)
                     ∘ᵥ Coequalizer.arr (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁))
                     triangle⊗∘arr²
 
-  triangle⊗ : Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ Unitorˡ⊗From {B = B₁})
+  triangle⊗ : Bimodhom.α (id-bimodule-hom {B = B₂} ⊗₁ unitorˡ-⊗-from {B = B₁})
               ∘ᵥ Bimodhom.α (associator-⊗-from {B₃ = B₂} {Id-Bimod} {B₁})
-              ≈ Bimodhom.α (Unitorʳ⊗From {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
+              ≈ Bimodhom.α (unitorʳ-⊗-from {B = B₂} ⊗₁ id-bimodule-hom {B = B₁})
 
   triangle⊗ = Coequalizer⇒Epi
                 (CoeqBimods (B₂ ⊗₀ Id-Bimod) B₁)
-                (Bimodhom.α (id-bimodule-hom ⊗₁ Unitorˡ⊗From)
+                (Bimodhom.α (id-bimodule-hom ⊗₁ unitorˡ-⊗-from)
                 ∘ᵥ Bimodhom.α associator-⊗-from)
-                (Bimodhom.α (Unitorʳ⊗From ⊗₁ id-bimodule-hom))
+                (Bimodhom.α (unitorʳ-⊗-from ⊗₁ id-bimodule-hom))
                 triangle⊗∘arr

src/Categories/Bicategory/Construction/Bimodules/Tensorproduct/Unitor/Naturality.agda

@@ -51,61 +51,61 @@ import Categories.Bicategory.Construction.Bimodules.Tensorproduct.Unitor
 module Left-Unitor-natural where
   open Bimodule B using (actionʳ)
   open Bimodule B' using () renaming (actionʳ to actionʳ')
-  open Unitor.Left-Unitor using (λ⇒⊗; triangle)
+  open Unitor.Left-Unitor using (λ⇒-⊗; triangle)
 
   abstract
-    λ⇒⊗-natural∘arr : (λ⇒⊗ {B'} ∘ᵥ Bimodhom.α (id-bimodule-hom ⊗₁ f)) ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B)
-                      ≈ (Bimodhom.α f ∘ᵥ λ⇒⊗ {B}) ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B)
-    λ⇒⊗-natural∘arr = begin
-      (λ⇒⊗ {B'} ∘ᵥ Bimodhom.α (id-bimodule-hom ⊗₁ f)) ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B) ≈⟨ assoc₂ ⟩
-      λ⇒⊗ {B'} ∘ᵥ Bimodhom.α (id-bimodule-hom ⊗₁ f) ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B)   ≈⟨ refl⟩∘⟨ ⟺ αSq-⊗ ⟩
-      λ⇒⊗ {B'} ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B') ∘ᵥ T₂ ▷ Bimodhom.α f                  ≈⟨ sym-assoc₂ ⟩
-      (λ⇒⊗ {B'} ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B')) ∘ᵥ T₂ ▷ Bimodhom.α f                ≈⟨ triangle {B'} ⟩∘⟨refl ⟩
+    λ⇒-⊗-natural∘arr : (λ⇒-⊗ {B'} ∘ᵥ Bimodhom.α (id-bimodule-hom ⊗₁ f)) ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B)
+                      ≈ (Bimodhom.α f ∘ᵥ λ⇒-⊗ {B}) ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B)
+    λ⇒-⊗-natural∘arr = begin
+      (λ⇒-⊗ {B'} ∘ᵥ Bimodhom.α (id-bimodule-hom ⊗₁ f)) ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B) ≈⟨ assoc₂ ⟩
+      λ⇒-⊗ {B'} ∘ᵥ Bimodhom.α (id-bimodule-hom ⊗₁ f) ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B)   ≈⟨ refl⟩∘⟨ ⟺ αSq-⊗ ⟩
+      λ⇒-⊗ {B'} ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B') ∘ᵥ T₂ ▷ Bimodhom.α f                  ≈⟨ sym-assoc₂ ⟩
+      (λ⇒-⊗ {B'} ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B')) ∘ᵥ T₂ ▷ Bimodhom.α f                ≈⟨ triangle {B'} ⟩∘⟨refl ⟩
       actionʳ' ∘ᵥ T₂ ▷ Bimodhom.α f                                           ≈⟨ linearʳ ⟩
       Bimodhom.α f ∘ᵥ actionʳ                                                 ≈⟨ refl⟩∘⟨ ⟺ (triangle {B}) ⟩
-      Bimodhom.α f ∘ᵥ λ⇒⊗ {B} ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B)                         ≈⟨ sym-assoc₂ ⟩
-      (Bimodhom.α f ∘ᵥ λ⇒⊗ {B}) ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B)                       ∎
+      Bimodhom.α f ∘ᵥ λ⇒-⊗ {B} ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B)                         ≈⟨ sym-assoc₂ ⟩
+      (Bimodhom.α f ∘ᵥ λ⇒-⊗ {B}) ∘ᵥ Coequalizer.arr (CoeqBimods Id-Bimod B)                       ∎
       where
         open hom.HomReasoning
         open Bimodhom f using (linearʳ)
         open TensorproductOfHomomorphisms id-bimodule-hom f using (αSq-⊗)
 
-    λ⇒⊗-natural : λ⇒⊗ {B'} ∘ᵥ Bimodhom.α (id-bimodule-hom ⊗₁ f) ≈ Bimodhom.α f ∘ᵥ λ⇒⊗ {B}
-    λ⇒⊗-natural = Coequalizer⇒Epi
+    λ⇒-⊗-natural : λ⇒-⊗ {B'} ∘ᵥ Bimodhom.α (id-bimodule-hom ⊗₁ f) ≈ Bimodhom.α f ∘ᵥ λ⇒-⊗ {B}
+    λ⇒-⊗-natural = Coequalizer⇒Epi
                     (CoeqBimods Id-Bimod B)
-                    (λ⇒⊗ ∘ᵥ Bimodhom.α (id-bimodule-hom ⊗₁ f))
-                    (Bimodhom.α f ∘ᵥ λ⇒⊗)
-                    λ⇒⊗-natural∘arr
+                    (λ⇒-⊗ ∘ᵥ Bimodhom.α (id-bimodule-hom ⊗₁ f))
+                    (Bimodhom.α f ∘ᵥ λ⇒-⊗)
+                    λ⇒-⊗-natural∘arr
 
   -- end abstract --
 
 module Right-Unitor-natural where
   open Bimodule B using (actionˡ)
   open Bimodule B' using () renaming (actionˡ to actionˡ')
-  open Unitor.Right-Unitor using (ρ⇒⊗; triangle)
+  open Unitor.Right-Unitor using (ρ⇒-⊗; triangle)
 
   abstract
-    ρ⇒⊗-natural∘arr : (ρ⇒⊗ {B'} ∘ᵥ Bimodhom.α (f ⊗₁ id-bimodule-hom)) ∘ᵥ Coequalizer.arr (CoeqBimods B Id-Bimod)
-                      ≈ (Bimodhom.α f ∘ᵥ ρ⇒⊗ {B}) ∘ᵥ Coequalizer.arr (CoeqBimods B Id-Bimod)
-    ρ⇒⊗-natural∘arr = begin
-      (ρ⇒⊗ {B'} ∘ᵥ Bimodhom.α (f ⊗₁ id-bimodule-hom)) ∘ᵥ Coequalizer.arr (CoeqBimods B Id-Bimod) ≈⟨ assoc₂ ⟩
-      ρ⇒⊗ {B'} ∘ᵥ Bimodhom.α (f ⊗₁ id-bimodule-hom) ∘ᵥ Coequalizer.arr (CoeqBimods B Id-Bimod)   ≈⟨ refl⟩∘⟨ ⟺ αSq-⊗ ⟩
-      ρ⇒⊗ {B'} ∘ᵥ Coequalizer.arr (CoeqBimods B' Id-Bimod) ∘ᵥ Bimodhom.α f ◁ T₁                  ≈⟨ sym-assoc₂ ⟩
-      (ρ⇒⊗ {B'} ∘ᵥ Coequalizer.arr (CoeqBimods B' Id-Bimod)) ∘ᵥ Bimodhom.α f ◁ T₁                ≈⟨ triangle {B'} ⟩∘⟨refl ⟩
+    ρ⇒-⊗-natural∘arr : (ρ⇒-⊗ {B'} ∘ᵥ Bimodhom.α (f ⊗₁ id-bimodule-hom)) ∘ᵥ Coequalizer.arr (CoeqBimods B Id-Bimod)
+                      ≈ (Bimodhom.α f ∘ᵥ ρ⇒-⊗ {B}) ∘ᵥ Coequalizer.arr (CoeqBimods B Id-Bimod)
+    ρ⇒-⊗-natural∘arr = begin
+      (ρ⇒-⊗ {B'} ∘ᵥ Bimodhom.α (f ⊗₁ id-bimodule-hom)) ∘ᵥ Coequalizer.arr (CoeqBimods B Id-Bimod) ≈⟨ assoc₂ ⟩
+      ρ⇒-⊗ {B'} ∘ᵥ Bimodhom.α (f ⊗₁ id-bimodule-hom) ∘ᵥ Coequalizer.arr (CoeqBimods B Id-Bimod)   ≈⟨ refl⟩∘⟨ ⟺ αSq-⊗ ⟩
+      ρ⇒-⊗ {B'} ∘ᵥ Coequalizer.arr (CoeqBimods B' Id-Bimod) ∘ᵥ Bimodhom.α f ◁ T₁                  ≈⟨ sym-assoc₂ ⟩
+      (ρ⇒-⊗ {B'} ∘ᵥ Coequalizer.arr (CoeqBimods B' Id-Bimod)) ∘ᵥ Bimodhom.α f ◁ T₁                ≈⟨ triangle {B'} ⟩∘⟨refl ⟩
       actionˡ' ∘ᵥ Bimodhom.α f ◁ T₁                                           ≈⟨ linearˡ ⟩
       Bimodhom.α f ∘ᵥ actionˡ                                                 ≈⟨ refl⟩∘⟨ ⟺ (triangle {B}) ⟩
-      Bimodhom.α f ∘ᵥ ρ⇒⊗ {B} ∘ᵥ Coequalizer.arr (CoeqBimods B Id-Bimod)                         ≈⟨ sym-assoc₂ ⟩
-      (Bimodhom.α f ∘ᵥ ρ⇒⊗ {B}) ∘ᵥ Coequalizer.arr (CoeqBimods B Id-Bimod)                       ∎
+      Bimodhom.α f ∘ᵥ ρ⇒-⊗ {B} ∘ᵥ Coequalizer.arr (CoeqBimods B Id-Bimod)                         ≈⟨ sym-assoc₂ ⟩
+      (Bimodhom.α f ∘ᵥ ρ⇒-⊗ {B}) ∘ᵥ Coequalizer.arr (CoeqBimods B Id-Bimod)                       ∎
       where
         open hom.HomReasoning
         open Bimodhom f using (linearˡ)
         open TensorproductOfHomomorphisms f id-bimodule-hom using (αSq-⊗)
 
-    ρ⇒⊗-natural : ρ⇒⊗ {B'} ∘ᵥ Bimodhom.α (f ⊗₁ id-bimodule-hom) ≈ Bimodhom.α f ∘ᵥ ρ⇒⊗ {B}
-    ρ⇒⊗-natural = Coequalizer⇒Epi
+    ρ⇒-⊗-natural : ρ⇒-⊗ {B'} ∘ᵥ Bimodhom.α (f ⊗₁ id-bimodule-hom) ≈ Bimodhom.α f ∘ᵥ ρ⇒-⊗ {B}
+    ρ⇒-⊗-natural = Coequalizer⇒Epi
                     (CoeqBimods B Id-Bimod)
-                    (ρ⇒⊗ ∘ᵥ Bimodhom.α (f ⊗₁ id-bimodule-hom))
-                    (Bimodhom.α f ∘ᵥ ρ⇒⊗)
-                    ρ⇒⊗-natural∘arr
+                    (ρ⇒-⊗ ∘ᵥ Bimodhom.α (f ⊗₁ id-bimodule-hom))
+                    (Bimodhom.α f ∘ᵥ ρ⇒-⊗)
+                    ρ⇒-⊗-natural∘arr
 
   -- end abstract --