Definition fromcompltoii2y (X Y : UU) (y : Y) : compl (coprod X Y) (ii2 y) -> coprod X (compl Y y). Proof. intros X0. induction X0 as [ t x ]. induction t as [ x0 | y0 ]. - apply (ii1 x0). - assert (ne : y != y0) by apply (negf (maponpaths (@ii2 _ _)) x). apply (ii2 (make_compl _ _ y0 ne)). Defined.