Change equiv-comp to comp-equiv (#1151)

The name `equiv-comp` was not in accordance with our general naming
scheme for compositions of maps, where often we name `comp` first, and
then the kind of morphism that the composition operation acts on.

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

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))
 ```