proposition: Theorem quotient_ump (B:HSet): (quotient R -> B) <~> (sig (fun f : A-> B => (forall a a0:A, R a a0 -> f a =f a0))).
proof: Proof. refine (equiv_adjointify (quotient_ump' B) (quotient_ump'' B) _ _). - intros [f Hf]. by apply equiv_path_sigma_hprop. - intros f. apply path_forall. red. apply quotient_ind_prop';[apply _|reflexivity]. Defined.
imports: HoTT.Basics HoTT.Types HSet TruncType Truncations.Core