proposition: Lemma atmost {X} {P : X -> Type}: (forall x, IsHProp (P x)) -> (atmost1P P) -> atmost1 (sig P).
proof: Proof. intros H H0 [x p] [y q]. specialize (H0 x y p q). induction H0. assert (H0: (p =q)) by apply path_ishprop. now induction H0. Qed.
imports: HoTT.Basics HoTT.Truncations.Core