proposition: Lemma isaprop_univalenceStatement : isaprop univalenceStatement.
proof: Proof. unfold univalenceStatement. apply impred_isaprop; intro X; apply impred_isaprop; intro Y. apply isapropisweq. Defined.
imports: UniMath.Foundations.PartD