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). intro y. unfold neqPred,negProp in neq_x; unfold isisolated in is. apply (iscontrweqb (weqtotal2overcoprod _)). induction (is y) as [eq|ne]. { induction eq. refine (iscontrweqf (weqii2withneg _ _) _). { intros z; induction z as [z e]; induction z as [z neq]; simpl in *. contradicts (!e) (negProp_to_neg neq). } { change x with (f (ii2 tt)). simple refine ((_,,_),,_). { exact tt. } { apply idpath. } { intro w. induction w as [t e]. unfold f in *; simpl in *. induction t. apply maponpaths. apply isaproppathsfromisolated. exact is. } } } { refine (iscontrweqf (weqii1withneg _ _) _). { intros z; induction z as [z e]; simpl in *. contradicts ne e. } { simple refine ((_,,_),,_). { exists y. apply neg_to_negProp. assumption. } { simpl. apply idpath. } intros z; induction z as [z e]; induction z as [z neq]; induction e; simpl in *. induction (proofirrelevance _ (pr1 (pr2 (neq_x z))) neq (neg_to_negProp ne)). apply idpath. } } Defined.
imports: UniMath.Foundations.All