fact: Definition Build_pHomotopy_pForall `{Funext} {A B : pType} {C : B -> pType} {f g : A ->* ppforall b, C b} (p : forall a, f a ==* g a) (q : p (point A) ==* phomotopy_path (point_eq f) @* (phomotopy_path (point_eq g))^*) : f ==* g.
imports: Basics Types Pointed.Core