{A : pType} {P : A -> pType} (f : ppforall (a : A), P a) : pmap_compose_ppforall (fun a => pmap_idmap) f ==* f. Proof. srapply Build_pHomotopy. + reflexivity. + symmetry. refine (whiskerR (concat_p1 _ @ ap_idmap _) _ @ concat_pV _). Defined.
Require Import Basics Types. Require Import Pointed.Core.