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