`{Funext} {A B : pType} {C : B -> pType} {f g : A ->* ppforall b, C b} (p : forall a, f a ==* g a) (q : p (point A) ==* phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*) : f ==* g. Proof. snrapply Build_pHomotopy. 1: intro a; exact (path_pforall (p a)). hnf; rapply moveR_equiv_M'. refine (_^ @ ap10 _ _). 2: exact path_equiv_path_pforall_phomotopy_path. apply path_pforall. refine (phomotopy_path_pp _ _ @* _ @* q^*). apply phomotopy_prewhisker. apply phomotopy_path_V. Defined.
Require Import Basics Types. Require Import Pointed.Core.