`{Funext} {A B C : pType} (f : B ->* A) (g : C ->* A) (t : B <~>* C) (h : f ==* g o* t) : pSect f <~> pSect g. Proof. srapply equiv_functor_sigma'. 1: exact (pequiv_pequiv_postcompose t). intro s; cbn. apply equiv_phomotopy_concat_l. refine ((pmap_compose_assoc _ _ _)^* @* _). apply pmap_prewhisker. exact h^*. Defined.
Require Import Basics Types Pointed.Core Pointed.pEquiv.