{X Y : Type} (f : X -> Y) (x1 x2 : X) : NullHomotopy f -> NullHomotopy (@ap _ _ f x1 x2). Proof. intros [y e]. unshelve eexists. - exact (e x1 @ (e x2)^). - intros p. apply moveL_pV. refine (concat_Ap e p @ _). refine (_ @ concat_p1 _); apply ap. apply ap_const. Defined.
Require Import HoTT.Basics. Require Import Types.Sigma.