{A B} : { equiv_rel : A -> B -> Type | { f : forall a, Contr { b : B & equiv_rel a b } | forall b, Contr { a : A & equiv_rel a b } } } <~> RelEquiv A B. Proof. issig. Defined.
Require Import HoTT.Basics HoTT.Types.