proposition: Theorem isweqrecompl (X : UU) (x : X) (is : isisolated X x) : isweq (recompl _ x).
proof: Proof. set (f := recompl _ x). set (g := invrecompl X x is). unfold invrecompl in g. simpl in g. assert (efg: ∏ x' : X, paths (f (g x')) x'). { intro. induction (is x') as [ x0 | e ]. - induction x0. unfold f. unfold g. simpl. unfold recompl. simpl. induction (is x) as [ x0 | e ]. + simpl. apply idpath. + induction (e (idpath x)). - unfold f. unfold g. simpl. unfold recompl. simpl. induction (is x') as [ x0 | e0 ]. + induction (e x0). + simpl. apply idpath. } assert (egf : ∏ u : coprod (compl X x) unit, paths (g (f u)) u). { unfold isisolated in is. intro. induction (is (f u)) as [ p | e ]. - induction u as [ c | u]. + simpl. induction c as [ t x0 ]. simpl in p. induction (x0 p). + induction u. assert (e1 : paths (g (f (ii2 tt))) (g x)). apply (maponpaths g p). assert (e2 : paths (g x) (ii2 tt)). { unfold g. induction (is x) as [ i | e ]. apply idpath. induction (e (idpath x)). } apply (pathscomp0 e1 e2). - induction u as [ c | u ]. simpl. induction c as [ t x0 ]. simpl. unfold isisolated in is. unfold g. induction (is t) as [ p | e0 ]. induction (x0 p). simpl in g. unfold f. unfold recompl. simpl in e. assert (ee : e0 = x0) by apply (proofirrelevance _ (isapropneg (x = t))). induction ee. apply idpath. unfold f. unfold g. simpl. induction u. induction (is x). + apply idpath. + induction (e (idpath x)). } apply (isweq_iso f g egf efg). Defined.
imports: UniMath.Foundations.PartB UniMath.Foundations.UnivalenceAxiom