`{Funext} {A B : pType} : pSect (@psnd A B) <~> (B ->* A). Proof. unfold pSect. transitivity {s : (B ->* A) * (B ->* B) & snd s ==* pmap_idmap}. { snrefine (equiv_functor_sigma' (equiv_pprod_coind (pfam_const A) (pfam_const B))^-1%equiv _). cbn. intro s. apply equiv_phomotopy_concat_l. srapply Build_pHomotopy. 1: reflexivity. cbn. apply moveL_pV. exact (concat_1p _ @ concat_p1 _). } snrefine (_ oE equiv_functor_sigma_id (fun s => equiv_path_pforall _ _)). snrefine (_ oE (equiv_functor_sigma_pb (equiv_sigma_prod0 _ _))^-1%equiv); cbn. refine (_ oE (equiv_sigma_assoc _ _)^-1%equiv). rapply equiv_sigma_contr. Defined.
Require Import Basics Types Pointed.Core Pointed.pEquiv.