Update src/foundation-core/whiskering-homotopies.lagda.md

Co-authored-by: Vojtěch Štěpančík <[email protected]>
UniMath · Dec 7, 2023 · 0c49117 · 0c49117
1 parent b40ebee
commit 0c49117
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/foundation-core/whiskering-homotopies.lagda.md b/src/foundation-core/whiskering-homotopies.lagda.md
@@ -246,7 +246,7 @@ module _
 
   ap-left-whisk-htpy :
     (h : {x : A} → B x → C x) {H H' : f ~ g} (α : H ~ H') → h ·l H ~ h ·l H'
-  ap-left-whisk-htpy h α x = ap (ap h) (α x)
+  ap-left-whisk-htpy h α x = (ap h) ·l α
 
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}