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