{ A B : pType } (f : A ->* B) : { s : B -> A & { p : s pt = pt & { H : f o s == idmap & H pt = ap f p @ (point_eq f) } } } <~> pSect f. Proof. transitivity {s : B -> A & {p : s pt = pt & {H : f o s == idmap & H pt = ap f p @ (point_eq f) @ 1 }}}. 2: make_equiv. do 3 (nrapply equiv_functor_sigma_id; intro). rapply equiv_concat_r. exact (concat_p1 _)^. Defined.
Require Import Basics Types Pointed.Core Pointed.pEquiv.