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