Lemma isdeceqcoprod {A B : UU} (h1 : isdeceq A) (h2 : isdeceq B) : isdeceq (A ⨿ B). Proof. intros ab ab'. induction ab as [a|b]; induction ab' as [a'|b']. - induction (h1 a a') as [p|p]. + apply inl, (maponpaths (@ii1 A B) p). + apply inr; intro H; apply (p (ii1_injectivity _ _ H)). - apply inr, negpathsii1ii2. - apply inr, negpathsii2ii1. - induction (h2 b b') as [p|p]. + apply inl, (maponpaths (@ii2 A B) p). + apply inr; intro H; apply (p (ii2_injectivity _ _ H)). Defined.