{A : pType} {P Q : A -> pType} {g g' : forall (a : A), P a ->* Q a} {f f' : ppforall (a : A), P a} (p : forall a, g a ==* g' a) (q : f ==* f') : pmap_compose_ppforall g f ==* pmap_compose_ppforall g' f'. Proof. srapply functor2_pforall_right. + exact p. + exact q. + exact (point_htpy (p (point A))). Defined.
Require Import Basics Types. Require Import Pointed.Core.