fact: Definition equiv_quotient_functor (f : A -> B) `{IsEquiv _ _ f} (fresp : forall x y, R x y <-> S (f x) (f y)) : Quotient R <~> Quotient S := Build_Equiv _ _ (Quotient_functor R S f (fun x y => fst (fresp x y))) _.
imports: Basics Types HSet TruncType Colimits.GraphQuotient Truncations.Core PropResizing