proposition: Theorem quotient_surjective: IsSurjection (class_of R).
proof: 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.
imports: HoTT.Basics HoTT.Types HSet TruncType Truncations.Core