{A : pType} {B B' : A -> pType} (g : forall a, B a ->* B' a) : pmap_compose_ppforall g (point_pforall B) ==* point_pforall B'. Proof. srapply Build_pHomotopy. + intro x. exact (point_eq (g x)). + exact (concat_p1 _ @ concat_1p _)^. Defined.
Require Import Basics Types. Require Import Pointed.Core.