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