(f : A -> B) `{IsEquiv _ _ f} (fresp : forall a b, R a b <-> S (f a) (f b)) : Quotient R <~> Quotient S := Build_Equiv _ _ (Quotient_functor R S f (fun a b => fst (fresp a b))) _.
Require Import Basics. Require Import Types. Require Import HSet. Require Import TruncType. Require Import Colimits.GraphQuotient. Require Import Truncations.Core.