proposition: Lemma isapropcomponent2 (P Q : UU) : isaprop (P ⨿ Q) -> isaprop Q.
proof: Proof. intros i. apply invproofirrelevance; intros q q'. exact (equality_by_case (proofirrelevance _ i (ii2 q) (ii2 q'))). Defined.
imports: UniMath.Foundations.PartA