Lemma isaprop_univalenceStatement : isaprop univalenceStatement. Proof. unfold univalenceStatement. apply impred_isaprop; intro X; apply impred_isaprop; intro Y. apply isapropisweq. Defined.
Require Import UniMath.Foundations.PartD.