fact: Definition pmap_compose_ppforall2_refl `{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 _.
imports: Basics Types Pointed.Core