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