fact: Definition 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.
imports: HoTT.Basics HoTT.Types HSet TruncType Truncations.Core