{A B} (e : RelEquiv A B) : A <~> B. Proof. refine (equiv_adjointify (fun a => (center { b : B & equiv_rel e a b}).1) (fun b => (center { a : A & equiv_rel e a b}).1) _ _); intro x; cbn. { refine (ap pr1 (contr _) : _.1 = (x; _).1). exact (center {a : A & equiv_rel e a x}).2. } { refine (ap pr1 (contr _) : _.1 = (x; _).1). exact (center {b : B & equiv_rel e x b}).2. } Defined.
Require Import HoTT.Basics HoTT.Types.