quotient_ump'' (B:HSet): (sig (fun f : A-> B => (forall a a0:A, R a a0 -> f a =f a0))) -> quotient R -> B.
Require Import HoTT.Basics HoTT.Types. Require Import HSet TruncType. Require Import Truncations.Core.