Update src/foundation-core/functoriality-function-types.lagda.md

Co-authored-by: Egbert Rijke <[email protected]>

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