diff --git a/src/foundation-core/functoriality-function-types.lagda.md b/src/foundation-core/functoriality-function-types.lagda.md
index 09a3767e332..7f14cbd6579 100644
--- a/src/foundation-core/functoriality-function-types.lagda.md
+++ b/src/foundation-core/functoriality-function-types.lagda.md
@@ -73,14 +73,14 @@ compute-htpy-precomp-refl-htpy :
 compute-htpy-precomp-refl-htpy f C h = eq-htpy-refl-htpy (h ∘ f)
 ```
 
-### Precomposition preserves composition of homotopies
+### Precomposition preserves concatenation of homotopies
 
 ```agda
-compute-comp-htpy-precomp :
+compute-concat-htpy-precomp :
   { l1 l2 l3 : Level} {A : UU l1} {B : UU l2}
   { f g h : A → B} (H : f ~ g) (K : g ~ h) (C : UU l3) →
   htpy-precomp (H ∙h K) C ~ (htpy-precomp H C ∙h htpy-precomp K C)
-compute-comp-htpy-precomp H K C k =
+compute-concat-htpy-precomp H K C k =
   ( ap
     ( eq-htpy)
     ( eq-htpy (distributive-left-whisk-concat-htpy k H K))) ∙