{A : Type} (P : A -> Type) `{Contr A} : { x : A & P x } <~> P (center A). Proof. refine (equiv_adjointify (fun xp => (contr xp.1)^ # xp.2) (fun p => (center A ; p)) _ _). - intros p; simpl. exact (ap (fun q => q # p) (path_contr _ 1)). - intros [a p]. refine (path_sigma' _ (contr a) _). apply transport_pV. Defined.
Require Import HoTT.Basics. Require Import Types.Arrow Types.Paths.