fix ap-left-whisk-htpy

UniMath · Dec 7, 2023 · c49e8a2 · c49e8a2
1 parent 0c49117
commit c49e8a2
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 h) ·l α
+  ap-left-whisk-htpy h α = (ap h) ·l α
 
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : A → UU l2} {C : (x : A) → B x → UU l3}