Lemma isolatedtoisolatedii1 (X Y : UU) (x : X) (is : isisolated _ x) : isisolated (coprod X Y) (ii1 x). Proof. intros. unfold isisolated. intro x'. induction x' as [ x0 | y ]. - induction (is x0) as [ p | e ]. + apply (ii1 (maponpaths (@ii1 X Y) p)). + apply (ii2 (negf (invmaponpathsincl (@ii1 X Y) (isinclii1 X Y) _ _) e)). - apply (ii2 (negpathsii1ii2 x y)). Defined.