Lemma isolatedtoisolatedii2 (X Y : UU) (y : Y) (is : isisolated _ y) : isisolated (coprod X Y) (ii2 y). Proof. intros. intro x'. induction x' as [ x | y0 ]. - apply (ii2 (negpathsii2ii1 x y)). - induction (is y0) as [ p | e ]. + apply (ii1 (maponpaths (@ii2 X Y) p)). + apply (ii2 (negf (invmaponpathsincl (@ii2 X Y) (isinclii2 X Y) _ _) e)). Defined.