diff --git a/src/foundation-core/equivalences.lagda.md b/src/foundation-core/equivalences.lagda.md
index 1f9549ab3a..44b0ec2c05 100644
--- a/src/foundation-core/equivalences.lagda.md
+++ b/src/foundation-core/equivalences.lagda.md
@@ -426,13 +426,13 @@ module _
     pr1 (is-equiv-comp g h (sh , rh) (sg , rg)) = section-comp g h sh sg
     pr2 (is-equiv-comp g h (sh , rh) (sg , rg)) = retraction-comp g h rg rh
 
-  equiv-comp : B ≃ X → A ≃ B → A ≃ X
-  pr1 (equiv-comp g h) = map-equiv g ∘ map-equiv h
-  pr2 (equiv-comp g h) = is-equiv-comp (pr1 g) (pr1 h) (pr2 h) (pr2 g)
+  comp-equiv : B ≃ X → A ≃ B → A ≃ X
+  pr1 (comp-equiv g h) = map-equiv g ∘ map-equiv h
+  pr2 (comp-equiv g h) = is-equiv-comp (pr1 g) (pr1 h) (pr2 h) (pr2 g)
 
   infixr 15 _∘e_
   _∘e_ : B ≃ X → A ≃ B → A ≃ X
-  _∘e_ = equiv-comp
+  _∘e_ = comp-equiv
 ```
 
 #### If a composite and its right factor are equivalences, then so is its left factor
diff --git a/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md b/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md
index b6009c687f..10609483e0 100644
--- a/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md
+++ b/src/synthetic-homotopy-theory/hatchers-acyclic-type.lagda.md
@@ -494,8 +494,7 @@ module _
       ( λ X →
         is-contr-equiv
           ( structure-Hatcher-Acyclic-Type (Ω X))
-          ( equiv-comp
-            ( equiv-pointed-map-Hatcher-Acyclic-Type A (Ω X) σ i)
+          ( ( equiv-pointed-map-Hatcher-Acyclic-Type A (Ω X) σ i) ∘e
             ( equiv-transpose-suspension-loop-adjunction A X))
           ( is-contr-structure-Hatcher-Acyclic-Type-Ω X))
 ```