{A : pType} {P Q R : A -> pType} (h : forall (a : A), Q a ->* R a) (g : forall (a : A), P a ->* Q a) (f : ppforall a, P a) : pmap_compose_ppforall (fun a => h a o* g a) f ==* pmap_compose_ppforall h (pmap_compose_ppforall g f). Proof. srapply Build_pHomotopy. + reflexivity. + simpl. refine ((whiskerL _ (inverse2 _)) @ concat_pV _)^. refine (whiskerR _ _ @ concat_pp_p _ _ _). refine (ap_pp _ _ _ @ whiskerR (ap_compose _ _ _)^ _). Defined.
Require Import Basics Types. Require Import Pointed.Core.