{B : Type} {sB : IsHSet B} (dclass : (forall x : A, B)) (dequiv : (forall x y, R x y -> dclass x = dclass y)) : quotient R -> B. Proof. apply (quotient_ind R (fun _ : quotient _ => B)) with dclass. intros ?? H'. destruct (related_classes_eq R H'). by apply dequiv. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Truncations.Core.