(f : A -> B) (fresp : forall x y, R x y <-> S (f x) (f y)) `{IsEquiv _ _ f} : quotient R <~> quotient S := Build_Equiv _ _ (quotient_functor R S f (fun x y => fst (fresp x y))) _.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Truncations.Core.