Lemma isaset_carrier_subset (X : hSet) (Y : hsubtype X) : isaset (∑ x, Y x). Proof. intros. apply isaset_total2. - apply setproperty. - intro x. apply isasetaprop, propproperty. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.