Rename and expand Assoc4 reasoning combinators

src/Categories/Adjoint/Construction/CoKleisli.agda

@@ -44,7 +44,7 @@ Forgetful =
    (F₁ (g ∘ F₁ f ∘ M.δ.η X)) ∘ M.δ.η X         ≈⟨ pushˡ trihom ⟩
    F₁ g ∘ (F₁ (F₁ f) ∘ F₁ (M.δ.η X)) ∘ M.δ.η X ≈⟨ refl⟩∘⟨ (pullʳ (sym M.assoc)) ⟩
    F₁ g ∘ F₁ (F₁ f) ∘ M.δ.η (F₀ X) ∘ M.δ.η X   ≈⟨ refl⟩∘⟨ pullˡ (sym (M.δ.commute f)) ⟩
-   F₁ g ∘ (M.δ.η Y ∘ F₁ f) ∘ M.δ.η X           ≈⟨ assoc²'' ⟩
+   F₁ g ∘ (M.δ.η Y ∘ F₁ f) ∘ M.δ.η X           ≈⟨ assoc²δγ ⟩
    (F₁ g ∘ M.δ.η Y) ∘ F₁ f ∘ M.δ.η X           ∎
 
 Cofree : Functor C (CoKleisli M)
@@ -146,4 +146,4 @@ Forgetful⊣Cofree =
     (M.ε.η B ∘ M.ε.η (F₀ B)) ∘ (F₁ (F₁ C.id) ∘ M.δ.η _) ≈⟨ assoc ⟩
     M.ε.η B ∘ (M.ε.η (F₀ B) ∘ (F₁ (F₁ C.id) ∘ M.δ.η _)) ≈⟨ refl⟩∘⟨ elim-center FF1≈1 ⟩
     M.ε.η B ∘ (M.ε.η (F₀ B) ∘ M.δ.η _)                  ≈⟨ elimʳ (Comonad.identityʳ M) ⟩
-    M.ε.η B                                             ∎
+    M.ε.η B                                             ∎

src/Categories/Adjoint/Construction/Kleisli.agda

@@ -113,14 +113,14 @@ module KleisliExtension where
   f-iso⇒Klf-iso {A} {B} f g (record { isoˡ = isoˡ ; isoʳ = isoʳ }) = record
     { isoˡ = begin
        (μ.η A ∘ F₁ g) ∘ μ.η B ∘ F₁ f           ≈⟨ center (sym (μ.commute g)) ⟩
-       μ.η A ∘ (μ.η (F₀ A) ∘ F₁ (F₁ g)) ∘ F₁ f ≈⟨ assoc²'' ○ pushˡ M.sym-assoc ⟩
+       μ.η A ∘ (μ.η (F₀ A) ∘ F₁ (F₁ g)) ∘ F₁ f ≈⟨ assoc²δγ ○ pushˡ M.sym-assoc ⟩
        μ.η A ∘ F₁ (μ.η A) ∘ F₁ (F₁ g) ∘ F₁ f   ≈⟨ refl⟩∘⟨ sym trihom ⟩
        μ.η A ∘ F₁ (μ.η A ∘ F₁ g ∘ f)           ≈⟨ refl⟩∘⟨ F-resp-≈ sym-assoc ⟩
        μ.η A ∘ F₁ ((μ.η A ∘ F₁ g) ∘ f)         ≈⟨ refl⟩∘⟨ F-resp-≈ isoʳ ○ M.identityˡ ⟩
        C.id                                        ∎
     ; isoʳ = begin
        (μ.η B ∘ F₁ f) ∘ μ.η A ∘ F₁ g           ≈⟨ center (sym (μ.commute f)) ⟩
-       μ.η B ∘ (μ.η (F₀ B) ∘ F₁ (F₁ f)) ∘ F₁ g ≈⟨ assoc²'' ○ pushˡ M.sym-assoc ⟩
+       μ.η B ∘ (μ.η (F₀ B) ∘ F₁ (F₁ f)) ∘ F₁ g ≈⟨ assoc²δγ ○ pushˡ M.sym-assoc ⟩
        μ.η B ∘ F₁ (μ.η B) ∘ F₁ (F₁ f) ∘ F₁ g   ≈⟨ refl⟩∘⟨ sym trihom ⟩
        μ.η B ∘ F₁ (μ.η B ∘ F₁ f ∘ g)           ≈⟨ refl⟩∘⟨ F-resp-≈ sym-assoc ⟩
        μ.η B ∘ F₁ ((μ.η B ∘ F₁ f) ∘ g)         ≈⟨ refl⟩∘⟨ F-resp-≈ isoˡ ○ M.identityˡ ⟩

src/Categories/Adjoint/Parametric.agda

@@ -82,7 +82,7 @@ record ParametricAdjoint {C D E : Category o ℓ e} (L : Functor C (Functors D E
               _ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ LL.F-resp-≈ a' R.homomorphism ⟩
               _ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ LL.homomorphism a' ⟩
               _ ≈⟨ refl⟩∘⟨ pullˡ (commute (L.₁ _) _) ⟩
-              _ ≈⟨ MR.assoc²'' E ⟩
+              _ ≈⟨  MR.assoc²δγ E  ⟩
               _ ∎ }
     ; F-resp-≈ = λ { {a , a'} {b , b'} {f} {g} (f≈g , f'≈g') →
         L.F-resp-≈ f'≈g' ⟩∘⟨ Functor.F-resp-≈ (L.₀ a') (R.F-resp-≈ f≈g)}

src/Categories/Category/Construction/CoKleisli.agda

@@ -52,7 +52,7 @@ CoKleisli {𝒞 = 𝒞} M =
   assoc′ : {A B C D : Obj} {f : F₀ A ⇒ B} {g : F₀ B ⇒ C} {h : F₀ C ⇒ D} → (h ∘ F₁ g ∘ δ.η B) ∘ F₁ f ∘ δ.η A ≈ h ∘ F₁ (g ∘ F₁ f ∘ δ.η A) ∘ δ.η A
   assoc′ {A} {B} {C} {D} {f} {g} {h} =
       begin
-        (h ∘ F₁ g ∘ δ.η B) ∘ (F₁ f ∘ δ.η A)             ≈⟨ assoc²' ⟩
+        (h ∘ F₁ g ∘ δ.η B) ∘ (F₁ f ∘ δ.η A)             ≈⟨ assoc²βε ⟩
         h ∘ (F₁ g ∘ (δ.η B ∘ (F₁ f ∘ δ.η A)))           ≈⟨ ((refl⟩∘⟨ (refl⟩∘⟨ sym assoc))) ⟩
         h ∘ (F₁ g ∘ ((δ.η B ∘ F₁ f) ∘ δ.η A))           ≈⟨ ((refl⟩∘⟨ (refl⟩∘⟨ pushˡ (δ.commute f)))) ⟩
         h ∘ (F₁ g ∘ (F₁ (F₁ f) ∘ (δ.η (F₀ A) ∘ δ.η A))) ≈⟨ refl⟩∘⟨ (refl⟩∘⟨  pushʳ (Comonad.assoc M)) ⟩
@@ -72,4 +72,4 @@ CoKleisli {𝒞 = 𝒞} M =
   identityʳ′ {A} {B} {f} = elimʳ (Comonad.identityˡ M)
 
   identity²′ : {A : Obj} → ε.η A ∘ F₁ (ε.η A) ∘ δ.η A ≈ ε.η A
-  identity²′ = elimʳ (Comonad.identityˡ M)
+  identity²′ = elimʳ (Comonad.identityˡ M)

src/Categories/Category/Construction/Functors.agda

@@ -168,7 +168,7 @@ uncurry {C₁ = C₁} {C₂ = C₂} {D = D} = record
                 _ ≈⟨ assoc ⟩
                 _ ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F.homomorphism ⟩
                 _ ≈⟨ refl⟩∘⟨ pullˡ (sym-commute (F.F₁ g1) f2) ⟩
-                _ ≈⟨ assoc²'' ⟩
+                _ ≈⟨ assoc²δγ ⟩
                 _ ∎ }
         ; F-resp-≈ = λ (f≈f₁ , f≈f₂) → F-resp-≈ (F.F₀ _) f≈f₂ ⟩∘⟨ F.F-resp-≈ f≈f₁
         } where module F = Functor F

src/Categories/Category/Construction/Properties/CoKleisli.agda

@@ -51,7 +51,7 @@ module _ {F : Functor 𝒞 𝒟} {G : Functor 𝒟 𝒞} (F⊣G : Adjoint F G) w
       G.F₁ g 𝒞.∘ G.F₁ ((F.F₁ (G.F₁ f)) 𝒟.∘ F.F₁ (unit.η (G.F₀ X))) 𝒞.∘ unit.η (G.F₀ X)      ≈⟨ (refl⟩∘⟨ pushˡ G.homomorphism) ⟩
       G.F₁ g 𝒞.∘ G.F₁ (F.F₁ (G.F₁ f)) 𝒞.∘ G.F₁ (F.F₁ (unit.η (G.F₀ X))) 𝒞.∘ unit.η (G.F₀ X) ≈⟨ (refl⟩∘⟨ (refl⟩∘⟨ sym (unit.commute (unit.η (G.F₀ X))))) ⟩
       G.F₁ g 𝒞.∘ G.F₁ (F.F₁ (G.F₁ f)) 𝒞.∘ unit.η (G.F₀ (F.F₀ (G.F₀ X))) 𝒞.∘ unit.η (G.F₀ X) ≈⟨ (refl⟩∘⟨ pullˡ (sym (unit.commute (G.F₁ f)))) ⟩
-      G.F₁ g 𝒞.∘ (unit.η (G.F₀ Y) 𝒞.∘ G.F₁ f) 𝒞.∘ unit.η (G.F₀ X)                           ≈⟨ MR.assoc²'' 𝒞 ⟩
+      G.F₁ g 𝒞.∘ (unit.η (G.F₀ Y) 𝒞.∘ G.F₁ f) 𝒞.∘ unit.η (G.F₀ X)                           ≈⟨ MR.assoc²δγ 𝒞 ⟩
       (G.F₁ g 𝒞.∘ unit.η (G.F₀ Y)) 𝒞.∘ G.F₁ f 𝒞.∘ unit.η (G.F₀ X)                           ∎
    ; F-resp-≈ = λ eq → 𝒞.∘-resp-≈ (G.F-resp-≈ eq) (Category.Equiv.refl 𝒞)
    }
@@ -93,4 +93,4 @@ module _ {F : Functor 𝒞 𝒟} {G : Functor 𝒟 𝒞} (F⊣G : Adjoint F G) w
     𝒞.id 𝒞.∘ G.F₁ (f 𝒟.∘ counit.η X) 𝒞.∘ unit.η (G.F₀ X)         ≈⟨ id-comm-sym ⟩
     (G.F₁ (f 𝒟.∘ counit.η X) 𝒞.∘ unit.η (G.F₀ X)) 𝒞.∘ 𝒞.id       ≈⟨ (pushˡ G.homomorphism ⟩∘⟨refl) ⟩
     (G.F₁ f 𝒞.∘ G.F₁ (counit.η X) 𝒞.∘ unit.η (G.F₀ X)) 𝒞.∘ 𝒞.id  ≈⟨ (elimʳ zag ⟩∘⟨refl) ⟩
-    G.F₁ f 𝒞.∘ 𝒞.id                                              ∎
+    G.F₁ f 𝒞.∘ 𝒞.id                                              ∎

src/Categories/Category/Monoidal/Braided/Properties.agda

@@ -85,7 +85,7 @@ private
                             ⟩
   braiding-coherence⊗unit = cancel-fromˡ braiding.FX≅GX (begin
     σ⇒ ∘ λ⇒ ⊗₁ id ∘ σ⇒ ⊗₁ id            ≈⟨ pullˡ (⟺ (glue◽◃ unitorˡ-commute-from coherence₁)) ⟩
-    (λ⇒ ∘ id ⊗₁ σ⇒ ∘ α⇒) ∘ σ⇒ ⊗₁ id     ≈⟨ assoc²' ⟩
+    (λ⇒ ∘ id ⊗₁ σ⇒ ∘ α⇒) ∘ σ⇒ ⊗₁ id     ≈⟨ assoc²βε ⟩
     λ⇒ ∘ id ⊗₁ σ⇒ ∘ α⇒ ∘ σ⇒ ⊗₁ id       ≈⟨ refl⟩∘⟨ hexagon₁ ⟩
     λ⇒ ∘ α⇒ ∘ σ⇒ ∘ α⇒                   ≈⟨ pullˡ coherence₁ ⟩
     λ⇒ ⊗₁ id ∘ σ⇒ ∘ α⇒                  ≈˘⟨ pushˡ (braiding.⇒.commute _) ⟩
@@ -168,7 +168,7 @@ assoc-reverse : [ X ⊗₀ (Y ⊗₀ Z) ⇒ (X ⊗₀ Y) ⊗₀ Z ]⟨
                 ≈ α⇐
                 ⟩
 assoc-reverse = begin
-  σ⇐ ∘ id ⊗₁ σ⇐ ∘ α⇒ ∘ σ⇒ ∘ id ⊗₁ σ⇒    ≈˘⟨ refl⟩∘⟨ assoc²' ⟩
+  σ⇐ ∘ id ⊗₁ σ⇐ ∘ α⇒ ∘ σ⇒ ∘ id ⊗₁ σ⇒    ≈⟨ refl⟩∘⟨ assoc²εβ ⟩
   σ⇐ ∘ (id ⊗₁ σ⇐ ∘ α⇒ ∘ σ⇒) ∘ id ⊗₁ σ⇒  ≈⟨ refl⟩∘⟨ pushˡ hex₁' ⟩
   σ⇐ ∘ (α⇒ ∘ σ⇒ ⊗₁ id) ∘ α⇐ ∘ id ⊗₁ σ⇒  ≈⟨ refl⟩∘⟨ pullʳ (sym-assoc ○ hexagon₂) ⟩
   σ⇐ ∘ α⇒ ∘ (α⇐ ∘ σ⇒) ∘ α⇐              ≈⟨ refl⟩∘⟨ pullˡ (cancelˡ associator.isoʳ) ⟩

src/Categories/Category/Monoidal/Interchange/Braided.agda

@@ -188,20 +188,20 @@ swapInner-assoc = begin
     α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐) ∘
     id ⊗₁ (id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐)) ∘ id ⊗₁ α⇒ ∘ α⇒ ∘
     (id ⊗₁ (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐)) ⊗₁ id ∘ α⇒ ⊗₁ id
-                                                                  ≈⟨ refl⟩∘⟨ merge₂ assoc²' ○ (refl⟩∘⟨ refl⟩∘⟨ assoc) ⟩∘⟨
+                                                                  ≈⟨ refl⟩∘⟨ merge₂ assoc²βε ○ (refl⟩∘⟨ refl⟩∘⟨ assoc) ⟩∘⟨
                                                                        refl⟩∘⟨ extendʳ assoc-commute-from ⟩
     α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐)) ∘
     id ⊗₁ α⇒ ∘
     id ⊗₁ ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id) ∘ α⇒ ∘ α⇒ ⊗₁ id
-                                                                  ≈⟨ refl⟩∘⟨ merge₂ (assoc²' ○ (refl⟩∘⟨ refl⟩∘⟨ assoc²')) ⟩∘⟨
+                                                                  ≈⟨ refl⟩∘⟨ merge₂ (assoc²βε ○ (refl⟩∘⟨ refl⟩∘⟨ assoc²βε)) ⟩∘⟨
                                                                        refl⟩∘⟨ switch-fromtoˡ (idᵢ ⊗ᵢ α) pentagon ⟩
     α⇐ ∘ id ⊗₁ (α⇒ ∘ α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘
     id ⊗₁ ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id) ∘ id ⊗₁ α⇐ ∘ α⇒ ∘ α⇒
                                                                   ≈˘⟨ refl⟩∘⟨ refl⟩∘⟨ pushˡ split₂ˡ ⟩
     α⇐ ∘ id ⊗₁
       (α⇒ ∘ α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒) ∘
     id ⊗₁ ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id ∘ α⇐) ∘ α⇒ ∘ α⇒
-                                                                  ≈⟨ refl⟩∘⟨ merge₂ assoc²' ○ (refl⟩∘⟨ refl⟩∘⟨ (assoc²' ○
+                                                                  ≈⟨ refl⟩∘⟨ merge₂ assoc²βε ○ (refl⟩∘⟨ refl⟩∘⟨ (assoc²βε ○
                                                                       (refl⟩∘⟨ refl⟩∘⟨ assoc))) ⟩∘⟨ Equiv.refl ⟩
     α⇐ ∘ id ⊗₁ (α⇒ ∘
       α⇒ ∘ (α⇐ ∘ α⇐) ⊗₁ id ∘ α⇐ ∘ id ⊗₁ (σ⇒ ⊗₁ id ∘ α⇐) ∘ α⇒ ∘
@@ -223,7 +223,7 @@ swapInner-assoc = begin
                                                                           pushʳ (refl⟩∘⟨ refl⟩⊗⟨ ⊗.identity ⟩∘⟨refl) ⟩
       α⇒ ∘ ((α⇐ ∘ α⇐) ∘ id ⊗₁ σ⇒) ⊗₁ id ∘ α⇒ ⊗₁ id ∘ α⇐ ∘
       (α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ (id ⊗₁ id) ∘ α⇐
-                                                                  ≈⟨ refl⟩∘⟨ merge₁ assoc² ⟩∘⟨ extendʳ assoc-commute-to ⟩
+                                                                  ≈⟨ refl⟩∘⟨ merge₁ assoc²αε ⟩∘⟨ extendʳ assoc-commute-to ⟩
       α⇒ ∘ (α⇐ ∘ α⇐ ∘ id ⊗₁ σ⇒ ∘ α⇒) ⊗₁ id ∘
       ((α⇒ ∘ σ⇒ ⊗₁ id ∘ α⇐) ⊗₁ id) ⊗₁ id ∘ α⇐ ∘ α⇐
                                                                   ≈˘⟨ refl⟩∘⟨ pushˡ split₁ˡ ⟩

src/Categories/Comonad/Construction/CoKleisli.agda

@@ -107,10 +107,9 @@ module _ (C : Category o ℓ e) where
 
       assoc' : {X Y Z : Obj} {k : F₀ X ⇒ Y} {l : F₀ Y ⇒ Z} → F₁ (l ∘ F₁ k ∘ δ.η X) ∘ δ.η X ≈ (F₁ l ∘ δ.η Y) ∘ F₁ k ∘ δ.η X
       assoc' {X} {Y} {Z} {k} {l} = begin
-        F₁ (l ∘ F₁ k ∘ δ.η X) ∘ δ.η X               ≈⟨ (homomorphism ⟩∘⟨refl) ⟩
-        ((F₁ l ∘ F₁ (F₁ k ∘ δ.η X) ) ∘ δ.η X)       ≈⟨ ((refl⟩∘⟨ homomorphism) ⟩∘⟨refl) ⟩
-        ((F₁ l ∘ (F₁ (F₁ k) ∘ F₁ (δ.η X))) ∘ δ.η X) ≈⟨ pullʳ (pullʳ M.sym-assoc) ⟩
-        (F₁ l ∘ F₁ (F₁ k) ∘ δ.η (F₀ X) ∘ δ.η X)     ≈⟨ (refl⟩∘⟨ (pullˡ (sym (δ.commute k)))) ⟩
-        (F₁ l ∘ (δ.η Y ∘ F₁ k) ∘ δ.η X)             ≈⟨ assoc²'' ⟩
-        (F₁ l ∘ δ.η Y) ∘ F₁ k ∘ δ.η X               ∎
-
+        F₁ (l ∘ F₁ k ∘ δ.η X) ∘ δ.η X             ≈⟨ homomorphism ⟩∘⟨refl ⟩
+        (F₁ l ∘ F₁ (F₁ k ∘ δ.η X) ) ∘ δ.η X       ≈⟨ (refl⟩∘⟨ homomorphism) ⟩∘⟨refl ⟩
+        (F₁ l ∘ (F₁ (F₁ k) ∘ F₁ (δ.η X))) ∘ δ.η X ≈⟨ pullʳ (pullʳ M.sym-assoc) ⟩
+        F₁ l ∘ F₁ (F₁ k) ∘ δ.η (F₀ X) ∘ δ.η X     ≈⟨ refl⟩∘⟨ pullˡ (sym (δ.commute k)) ⟩
+        F₁ l ∘ (δ.η Y ∘ F₁ k) ∘ δ.η X             ≈⟨ assoc²δγ ⟩
+        (F₁ l ∘ δ.η Y) ∘ F₁ k ∘ δ.η X             ∎

src/Categories/Diagram/End/Properties.agda

@@ -111,11 +111,11 @@ module _ {P Q : Functor (Product (Category.op C) C) D} (P⇒Q : NaturalTransform
       { α = λ c → η (c , c) ∘ dinatural.α ep c
       ; commute = λ {C} {C′} f → begin
         Q.₁ (C.id , f) ∘ (η (C , C) ∘ αp C) ∘ D.id       ≈⟨ pullˡ sym-assoc ⟩
-        ((Q.₁ (C.id , f) ∘ η (C , C)) ∘ αp C) ∘ D.id     ≈⟨ (nt.sym-commute (C.id , f) ⟩∘⟨refl ⟩∘⟨refl) ⟩
-        ((η (C , C′) ∘ P.₁ (C.id , f)) ∘ αp C) ∘ D.id    ≈⟨ assoc² ⟩
-        η (C , C′) ∘ (P.₁ (C.id , f) ∘ αp C ∘ D.id)      ≈⟨ (refl⟩∘⟨ αp-comm f) ⟩
-        η (C , C′) ∘ P.₁ (f , C.id) ∘ αp C′ ∘ D.id       ≈˘⟨ assoc² ⟩
-        ((η (C , C′) ∘ P.₁ (f , C.id)) ∘ αp C′) ∘ D.id   ≈⟨ (nt.commute (f , C.id) ⟩∘⟨refl ⟩∘⟨refl) ⟩
+        ((Q.₁ (C.id , f) ∘ η (C , C)) ∘ αp C) ∘ D.id     ≈⟨ nt.sym-commute (C.id , f) ⟩∘⟨refl ⟩∘⟨refl ⟩
+        ((η (C , C′) ∘ P.₁ (C.id , f)) ∘ αp C) ∘ D.id    ≈⟨ assoc²αε ⟩
+        η (C , C′) ∘ (P.₁ (C.id , f) ∘ αp C ∘ D.id)      ≈⟨ refl⟩∘⟨ αp-comm f ⟩
+        η (C , C′) ∘ P.₁ (f , C.id) ∘ αp C′ ∘ D.id       ≈⟨ assoc²εα ⟩
+        ((η (C , C′) ∘ P.₁ (f , C.id)) ∘ αp C′) ∘ D.id   ≈⟨ nt.commute (f , C.id) ⟩∘⟨refl ⟩∘⟨refl ⟩
         ((Q.₁ (f , C.id) ∘ η (C′ , C′)) ∘ αp C′) ∘ D.id  ≈⟨ pushˡ assoc ⟩
         Q.₁ (f , C.id) ∘ (η (C′ , C′) ∘ αp C′) ∘ D.id    ∎
       }

src/Categories/Diagram/Limit/Ran.agda

@@ -169,7 +169,7 @@ module _ {o ℓ e o′ ℓ′ e′ o″ ℓ″ e″} {C : Category o′ ℓ′ e
         ; commute = λ {K} → begin
           ⊤Gd.proj W K ∘ R₁ g ∘ R₁ f        ≈⟨ pullˡ (proj-red K g) ⟩
           ⊤Gd.proj Z (↙⇒ K g) ∘ R₁ f       ≈⟨ proj-red (↙⇒ K g) f ⟩
-          ⊤Gd.proj Y (↙⇒ (↙⇒ K g) f)     ≈⟨ proj≈ (D.Equiv.trans D.identityˡ (MR.assoc²' D)) ⟩
+          ⊤Gd.proj Y (↙⇒ (↙⇒ K g) f)     ≈⟨ proj≈ (D.Equiv.trans D.identityˡ (MR.assoc²βε D)) ⟩
           ⊤Gd.proj Y (↙⇒ K (g D.∘ f))      ∎
         }
 

src/Categories/Functor/Hom.agda

@@ -30,7 +30,7 @@ module Hom {o ℓ e} (C : Category o ℓ e) where
         ; cong = ∘-resp-≈ʳ ∙ ∘-resp-≈ˡ
         }
     ; identity     = identityˡ ○ identityʳ
-    ; homomorphism = refl⟩∘⟨ sym-assoc ○ ⟺ assoc²''
+    ; homomorphism = ∘-resp-≈ʳ sym-assoc ○ assoc²γδ
     ; F-resp-≈     = λ { (f₁≈g₁ , f₂≈g₂) → f₂≈g₂ ⟩∘⟨ refl⟩∘⟨ f₁≈g₁}
     }
     where F₀′ : Obj × Obj → Setoid ℓ e

src/Categories/Functor/Profunctor.agda

@@ -316,7 +316,7 @@ module _ {o ℓ e} {o′} (C : Category o ℓ e) (D : Category o′ ℓ e) where
     module C = Category C
     open module D = Category D hiding (id)
     open D.HomReasoning
-    open import Categories.Morphism.Reasoning D using (assoc²''; elimˡ; elimʳ)
+    open import Categories.Morphism.Reasoning D using (assoc²γδ; elimˡ; elimʳ)
 
   -- representable profunctors
   -- hom(f,1)
@@ -338,7 +338,7 @@ module _ {o ℓ e} {o′} (C : Category o ℓ e) (D : Category o′ ℓ e) where
     ; homomorphism = λ { {f = f0 , f1} {g = g0 , g1} {x} → begin
         (g1 ∘ f1) ∘ x ∘ F₁ (f0 C.∘ g0)  ≈⟨ refl⟩∘⟨ refl⟩∘⟨ F.homomorphism ⟩
         (g1 ∘ f1) ∘ x ∘ F₁ f0 ∘ F₁ g0   ≈⟨ refl⟩∘⟨ D.sym-assoc ⟩
-        (g1 ∘ f1) ∘ (x ∘ F₁ f0) ∘ F₁ g0 ≈⟨ Equiv.sym assoc²'' ⟩
+        (g1 ∘ f1) ∘ (x ∘ F₁ f0) ∘ F₁ g0 ≈⟨ assoc²γδ ⟩
         g1 ∘ (f1 ∘ x ∘ F₁ f0) ∘ F₁ g0   ∎
       }
     ; F-resp-≈ = λ { {f = f0 , f1} {g = g0 , g1} (f0≈g0 , f1≈g1) {x} → begin
@@ -368,7 +368,7 @@ module _ {o ℓ e} {o′} (C : Category o ℓ e) (D : Category o′ ℓ e) where
     ; homomorphism = λ { {f = f0 , f1} {g = g0 , g1} {x} → begin
         F₁ (g1 C.∘ f1) ∘ x ∘ f0 ∘ g0    ≈⟨ F.homomorphism ⟩∘⟨refl ⟩
         (F₁ g1 ∘ F₁ f1) ∘ x ∘ f0 ∘ g0   ≈⟨ refl⟩∘⟨ D.sym-assoc ⟩
-        (F₁ g1 ∘ F₁ f1) ∘ (x ∘ f0) ∘ g0 ≈⟨ Equiv.sym assoc²'' ⟩
+        (F₁ g1 ∘ F₁ f1) ∘ (x ∘ f0) ∘ g0 ≈⟨ assoc²γδ ⟩
         F₁ g1 ∘ (F₁ f1 ∘ x ∘ f0) ∘ g0   ∎
       }
     ; F-resp-≈ = λ { {f = f0 , f1} {g = g0 , g1} (f0≈g0 , f1≈g1) {x} → begin

src/Categories/Functor/Properties.agda

@@ -137,13 +137,13 @@ module _ (F : Functor C D) where
           (⟨f⟩ , q) = full (_≅_.to sb ∘ f ∘ _≅_.from sa)
           (⟨g⟩ , r) = full (_≅_.to sc ∘ g ∘ _≅_.from sb)
       in faith $ begin
-        F₁ ⟨g∘f⟩                                                         ≈⟨ p ⟩
-        _≅_.to sc ∘ (g ∘ f) ∘ _≅_.from sa                               ≈⟨ assoc²'' ⟩
+        F₁ ⟨g∘f⟩                                                        ≈⟨ p ⟩
+        _≅_.to sc ∘ (g ∘ f) ∘ _≅_.from sa                               ≈⟨ assoc²δγ ⟩
         (_≅_.to sc ∘ g) ∘ (f ∘ _≅_.from sa)                             ≈⟨ insertInner (_≅_.isoʳ sb) ⟩
         ((_≅_.to sc ∘ g) ∘ _≅_.from sb) ∘ (_≅_.to sb ∘ f ∘ _≅_.from sa) ≈⟨ D.assoc ⟩∘⟨refl ⟩
         (_≅_.to sc ∘ g ∘ _≅_.from sb) ∘ (_≅_.to sb ∘ f ∘ _≅_.from sa)   ≈˘⟨ (r ⟩∘⟨ q ) ⟩
-        F₁ ⟨g⟩ ∘ F₁ ⟨f⟩                                                   ≈˘⟨ homomorphism ⟩
-        F₁ (⟨g⟩ C.∘ ⟨f⟩)                                                  ∎
+        F₁ ⟨g⟩ ∘ F₁ ⟨f⟩                                                 ≈˘⟨ homomorphism ⟩
+        F₁ (⟨g⟩ C.∘ ⟨f⟩)                                                ∎
     ; F-resp-≈ = λ {X} {Y} {f} {g} f≈g →
       let sa = proj₂ (surj X)
           sb = proj₂ (surj Y)

src/Categories/Monad/Construction/Kleisli.agda

@@ -111,7 +111,7 @@ module _ (C : Category o ℓ e) where
         (μ.η Z ∘ F₁ (μ.η Z ∘ ₁ l) ∘ F₁ k)           ≈⟨ refl⟩∘⟨ homomorphism ⟩∘⟨refl ⟩ 
         (μ.η Z ∘ (F₁ (μ.η Z) ∘ F₁ (F₁ l)) ∘ F₁ k)   ≈⟨ pullˡ (pullˡ M.assoc) ⟩ 
         (((μ.η Z ∘ μ.η (F₀ Z)) ∘ F₁ (F₁ l)) ∘ F₁ k) ≈⟨ pullʳ (μ.commute l) ⟩∘⟨refl ⟩
-        (μ.η Z ∘ F₁ l ∘ μ.η Y) ∘ F₁ k               ≈⟨ trans assoc²' sym-assoc ⟩
+        (μ.η Z ∘ F₁ l ∘ μ.η Y) ∘ F₁ k               ≈⟨ assoc²βγ ⟩
         (μ.η Z ∘ F₁ l) ∘ μ.η Y ∘ F₁ k               ∎