{A : Type} (a : A) (P : A -> Type) (Prefl : P a) (cp : Contr {y:A & P y} ) (b : A) : P b <~> a = b. Proof. apply equiv_inverse. srefine (Build_Equiv _ _ _ _). { intros []; apply Prefl. } revert b; apply isequiv_from_functor_sigma. rapply isequiv_contr_contr. Defined.
Require Import Basics. Require Import Types.Sigma Types.Equiv Types.Paths. Require Import HoTT.Tactics.