proposition: Theorem equiv_quotient_ump (B : HSet) : (A / R -> B) <~> {f : A -> B & forall x y, R x y -> f x = f y}.
proof: Proof. srapply equiv_adjointify. + intro f. exists (compose f (class_of R)). intros; f_ap. by apply qglue. + intros [f H']. apply (Quotient_rec _ _ _ H'). + intros [f Hf]. by apply equiv_path_sigma_hprop. + intros f. apply path_forall. srapply Quotient_ind_hprop. reflexivity. Defined.
imports: Basics Types HSet TruncType Colimits.GraphQuotient Truncations.Core PropResizing