proposition: Theorem isweqrecompl_ne (X : UU) (x : X) (is : isisolated X x) (neq_x : neqPred x) : isweq (recompl_ne _ x neq_x).
proof: 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.
imports: UniMath.Foundations.All