IsSurjection (class_of R). Proof. apply BuildIsSurjection. apply (quotient_ind_prop (fun y => merely (hfiber (class_of R) y))); try exact _. intro x. apply tr. by exists x. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Truncations.Core.