`{Funext} {A : pType} {P Q : A -> pType} (g : forall (a : A), P a ->* Q a) (f : ppforall (a : A), P a) : pmap_compose_ppforall2 (fun a => phomotopy_reflexive (g a)) (phomotopy_reflexive f) ==* phomotopy_reflexive _. Proof. unfold pmap_compose_ppforall2. revert Q g. refine (fiberwise_pointed_map_rec _ _). intros Q g. srapply functor2_pforall_right_refl. Defined.
Require Import Basics Types. Require Import Pointed.Core.