fact: Definition issig_relequiv {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.
imports: HoTT.Basics HoTT.Types