proposition: Lemma isProofIrrelevant_paths {X} (irr:isProofIrrelevant X) {x y:X} : isProofIrrelevant (x=y).
proof: Proof. intros p q. assert (r := invproofirrelevance X irr x y). exact (pr2 r p @ ! pr2 r q). Defined.
imports: UniMath.Foundations.PartA