quotient_functor_equiv' (f : A <~> B) (fresp : forall x y, R x y <-> S (f x) (f y)) : quotient R <~> quotient S := quotient_functor_equiv f fresp.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Truncations.Core.