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