{A B : Type} `{Contr A} `{Contr B} : (A <~> B) := Build_Equiv _ _ (fun _ => center B) _. Global Instance isequiv_pr1 {A : Type} (P : A -> Type) `{forall x, Contr (P x)} : IsEquiv (@pr1 A P). Proof. apply (Build_IsEquiv _ _ (@pr1 A P) (fun x => (x ; center (P x))) (fun x => 1) (fun xy => match xy with | exist x y => ap (exist _ x) (contr _) end)). intros [x y]. rewrite <- ap_compose. symmetry; apply ap_const. Defined.
Require Import