Lemma isapropcoprod (P Q : UU) : isaprop P -> isaprop Q -> (P -> Q -> ∅) -> isaprop (P ⨿ Q). Proof. intros i j n. apply invproofirrelevance. intros a b. apply inv_equality_by_case. induction a as [a|a]. - induction b as [b|b]. + apply i. + contradicts (n a) b. - induction b as [b|b]. + contradicts (n b) a. + apply j. Defined.