Theorem isweqtocompltoii2y (X Y : UU) (y : Y) : isweq (tocompltoii2y X Y y). Proof. intros. set (f := tocompltoii2y X Y y). set (g := fromcompltoii2y X Y y). assert (egf : ∏ nexy : _, paths (g (f nexy)) nexy). { intro. induction nexy as [ x | c ]. - apply idpath. - induction c as [ t x ]. simpl. assert (e : paths (negf (maponpaths (@ii2 X Y)) (negf (invmaponpathsincl (@ii2 X Y) (isinclii2 X Y) y t) x)) x) by apply (isapropneg (y = t)). apply (maponpaths (fun ee : y != t => ii2 (make_compl _ y t ee)) e). } assert (efg : ∏ neii2x : _, paths (f (g neii2x)) neii2x). { intro. induction neii2x as [ t x ]. induction t as [ x0 | y0 ]. - simpl. assert (e : (negpathsii2ii1 x0 y) = x) by apply (isapropneg (paths _ _)). apply (maponpaths (fun ee : (neg (paths (ii2 y) (ii1 x0))) => (make_compl _ _ (ii1 x0) ee)) e). - simpl. assert (e : paths (negf (invmaponpathsincl _ (isinclii2 X Y) y y0) (negf (maponpaths (@ii2 X Y)) x)) x) by apply (isapropneg (paths _ _)). apply (maponpaths (fun ee : (neg (paths (ii2 y) (ii2 y0))) => (make_compl _ _ (ii2 y0) ee)) e). } apply (isweq_iso f g egf efg). Defined.