Lemma isaprop_istotal {X : hSet} (R : hrel X) : isaprop (istotal R). Proof. intros. unfold istotal. apply impred; intro x. apply impred; intro y. apply propproperty. Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.