proposition: Lemma isaset_carrier_subset (X : hSet) (Y : hsubtype X) : isaset (∑ x, Y x).
proof: Proof. intros. apply isaset_total2. - apply setproperty. - intro x. apply isasetaprop, propproperty. Defined.
imports: UniMath.Foundations.Propositions