proposition: Lemma isaprop_isProofIrrelevant X : isaprop (isProofIrrelevant X).
proof: Proof. intros. apply invproofirrelevance. intros i j. apply funextsec; intro x; apply funextsec; intro y. generalize (i x y) as p; generalize (j x y) as q; intros. apply isProofIrrelevant_paths. assumption. Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom