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