Lemma isaprop_propositionalUnivalenceStatement : isaprop propositionalUnivalenceStatement. 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.
Require Import UniMath.Foundations.PartD.