Definition tocompltoii2y (X Y : UU) (y : Y) : coprod X (compl Y y) -> compl (coprod X Y) (ii2 y). Proof. intros X0. induction X0 as [ x | c ]. - split with (ii1 x). apply (negpathsii2ii1 x y). - split with (ii2 (pr1 c)). assert (e : neg(y = (pr1 c))) by apply (pr2 c). apply (negf (invmaponpathsincl (@ii2 _ _) (isinclii2 X Y) _ _) e). Defined.