fact: Definition pmap_compose_ppforall2_left {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).
imports: Basics Types Pointed.Core