Theorem isweqrecompl_ne (X : UU) (x : X) (is : isisolated X x) (neq_x : neqPred x) : isweq (recompl_ne _ x neq_x). Proof. intros. set (f := recompl_ne X x neq_x). set (g := invrecompl_ne X x neq_x is). refine (isweq_iso f g _ _). {intro u. induction (is (f u)) as [ eq | ne ]. - induction u as [ c | u]. + simpl. induction c as [ t neq ]; simpl; simpl in eq. contradicts (negProp_to_neg neq) eq. + induction u. intermediate_path (g x). {apply maponpaths. exact (pathsinv0 eq). } {unfold g, invrecompl_ne. induction (is x) as [ i | e ]. {apply idpath. } {simpl. contradicts e (idpath x). }} - induction u as [ c | u ]. simpl. + induction c as [ y neq ]; simpl. unfold g, invrecompl_ne. induction (is y) as [ eq' | ne' ]. {contradicts (negProp_to_neg neq) eq'. } {induction (ii2 ne') as [eq|neq']. {simpl. contradicts eq ne'. } {simpl. apply maponpaths. unfold make_compl_ne. apply maponpaths. apply proofirrelevance. exact (pr1 (pr2 (neq_x y))). }} + induction u. unfold f,g,invrecompl_ne;simpl. induction (is x) as [eq|neq]. {simpl. apply idpath. } {apply fromempty. apply neq. apply idpath. }} {intro y. unfold f,g,invrecompl_ne;simpl. induction (is y) as [eq|neq]. - induction eq. apply idpath. - simpl. apply idpath. } Defined.