{B : HSet} {dclass : (A -> A -> B)}: forall dequiv : (forall x x', R x x' -> forall y y', R y y' -> dclass x y = dclass x' y'), quotient R -> quotient R -> B. Proof. intro. assert (dequiv0 : forall x x0 y : A, R x0 y -> dclass x x0 = dclass x y) by (intros ? ? ? Hx; apply dequiv;[apply Hrefl|done]). refine (quotient_rec (fun x => quotient_rec (dclass x) (dequiv0 x)) _). intros x x' Hx. apply path_forall. red. assert (dequiv1 : forall y : A, quotient_rec (dclass x) (dequiv0 x) (class_of _ y) = quotient_rec (dclass x') (dequiv0 x') (class_of _ y)) by (intros; by apply dequiv). refine (quotient_ind R (fun q => quotient_rec (dclass x) (dequiv0 x) q = quotient_rec (dclass x') (dequiv0 x') q) dequiv1 _). intros. apply path_ishprop. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Truncations.Core.