proposition: Lemma isaprop_propositionalUnivalenceStatement : isaprop propositionalUnivalenceStatement.
proof: Proof. unfold propositionalUnivalenceStatement. apply impred_isaprop; intro P; apply impred_isaprop; intro Q; apply impred_isaprop; intro i; apply impred_isaprop; intro j; apply impred_isaprop; intros _; apply impred_isaprop; intros _. apply (isofhlevelweqb 1 (univalence P Q)). fold isaprop. apply isapropweqtoprop. exact j. Defined.
imports: UniMath.Foundations.PartD