`{Funext} {A : pType} {P Q : A -> pType} (g : forall a, P a ->* Q a) {f f' : ppforall a, P a} (p : f ==* f') : ap (pmap_compose_ppforall g) (path_pforall p) = path_pforall (pmap_compose_ppforall2_right g p). Proof. revert f' p. refine (phomotopy_ind _ _). refine (ap _ path_pforall_1 @ path_pforall_1^ @ ap _ _^). exact (path_pforall (pmap_compose_ppforall2_refl _ _)). Defined.
Require Import Basics Types. Require Import Pointed.Core.