proposition: Lemma type_equiv_contr `{Univalence} {A : Type@{i}} : A <~> {P : A -> Type | Contr {x : A & P x}}.
proof: Proof. apply equiv_inverse; unshelve eapply equiv_adjointify. - move=> [F [[a ?] ?]]; exact a. - by move=> a; exists (paths a); apply contr_basedpaths. - done. - move=> [P Pc]; unshelve eapply path_sigma. { apply: path_arrow => a; apply: equiv_path_universe. apply: equiv_inverse; apply: equiv_path_from_contr. by case: Pc => -[]. } by apply: path_contr. Defined.
imports: Coq(ssreflect)