{X} (P:X-> Type): (forall x, IsHProp (P x)) -> (hunique P) -> sig P. Proof. intros H1 [H H0]. apply (@Trunc_rec (-1) (sig P) );auto. by apply hprop_allpath, atmost. Qed.
Require Import HoTT.Basics HoTT.Truncations.Core.