{-# OPTIONS --no-load-primitives --cubical #-} module CubicalHott.Chapter2Lemma221 where open import CubicalHott.Chapter1
Lemma 2.2.1
ap : {l1 l2 : Level} {A : Type l1} {B : Type l2} {x y : A} → (f : A → B) → (p : x ≡ y) → f x ≡ f y ap {l1} {l2} {A} {B} {x} {y} f p i = f (p i)