From c49e8a22e883c0278b1d5402fb990992d1ee1489 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Thu, 7 Dec 2023 23:53:43 +0100 Subject: [PATCH] fix `ap-left-whisk-htpy` --- src/foundation-core/whiskering-homotopies.lagda.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/foundation-core/whiskering-homotopies.lagda.md b/src/foundation-core/whiskering-homotopies.lagda.md index 0e20ef65f7..5aeb7fdd6b 100644 --- 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}