{A : pType} {P Q : A -> pType} {g g' : forall (a : A), P a ->* Q a} (f : ppforall (a : A), P a) (p : forall a, g a ==* g' a) : pmap_compose_ppforall g f ==* pmap_compose_ppforall g' f := pmap_compose_ppforall2 p (phomotopy_reflexive f).
Require Import Basics Types. Require Import Pointed.Core.