Martin Escardo, 21 March 2018, 1st December 2019.

We prove the known (constructive) fact that

  X + πŸ™ ≃ Y + πŸ™ β†’ X ≃ Y.

The new proof from 1st December 2019 is extracted from the module
UF.Factorial and doesn't use function extensionality. The old proof
from 21 March 2018 is included at the end.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module Factorial.PlusOneLC where

open import Factorial.Swap
open import MLTT.Plus-Properties
open import MLTT.Spartan
open import UF.DiscreteAndSeparated
open import UF.Equiv
open import UF.Retracts

+πŸ™-cancellable : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
               β†’ (X + πŸ™ {𝓦} ≃ Y + πŸ™ {𝓣})
               β†’ X ≃ Y
+πŸ™-cancellable {𝓀} {π“₯} {𝓦} {𝓣} {X} {Y} (Ο† , i) = qinveq f' (g' , Ξ·' , Ξ΅')
 where
  zβ‚€ : X + πŸ™
  zβ‚€ = inr ⋆

  tβ‚€ : Y + πŸ™
  tβ‚€ = inr ⋆

  j : is-isolated zβ‚€
  j = new-point-is-isolated

  k : is-isolated (Ο† zβ‚€)
  k = equivs-preserve-isolatedness Ο† i zβ‚€ j

  l : is-isolated tβ‚€
  l = new-point-is-isolated

  s : Y + πŸ™ β†’ Y + πŸ™
  s = swap (Ο† zβ‚€) tβ‚€ k l

  f : X + πŸ™ β†’ Y + πŸ™
  f = s ∘ Ο†

  p : f zβ‚€ ＝ tβ‚€
  p = swap-equationβ‚€ (Ο† zβ‚€) tβ‚€ k l

  g : Y + πŸ™ β†’ X + πŸ™
  g = inverse Ο† i ∘ s

  h : s ∘ s ∼ id
  h = swap-involutive (Ο† zβ‚€) tβ‚€ k l

  η : g ∘ f ∼ id
  Ξ· z = inverse Ο† i (s (s (Ο† z))) ＝⟨ ap (inverse Ο† i) (h (Ο† z)) ⟩
        inverse Ο† i (Ο† z)         ＝⟨ inverses-are-retractions Ο† i z ⟩
        z                         ∎

  Ρ : f ∘ g ∼ id
  Ξ΅ t = s (Ο† (inverse Ο† i (s t))) ＝⟨ ap s (inverses-are-sections Ο† i (s t)) ⟩
        s (s t)                   ＝⟨ h t ⟩
        t                         ∎

  f' : X β†’ Y
  f' x = pr₁ (inl-preservation f p (sections-are-lc f (g , Ξ·)) x)

  a : (x : X) β†’ f (inl x) ＝ inl (f' x)
  a x = prβ‚‚ (inl-preservation f p (sections-are-lc f (g , Ξ·)) x)

  q = g tβ‚€     ＝⟨ ap g (p ⁻¹) ⟩
      g (f zβ‚€) ＝⟨ Ξ· zβ‚€ ⟩
      inr ⋆    ∎

  g' : Y β†’ X
  g' y = pr₁ (inl-preservation g q (sections-are-lc g (f , Ξ΅)) y)

  b : (y : Y) β†’ g (inl y) ＝ inl (g' y)
  b y = prβ‚‚ (inl-preservation g q (sections-are-lc g (f , Ξ΅)) y)

  Ξ·' : (x : X) β†’ g' (f' x) ＝ x
  η' x = inl-lc (inl (g' (f' x)) ＝⟨ (b (f' x))⁻¹ ⟩
                 g (inl (f' x))  ＝⟨ (ap g (a x))⁻¹ ⟩
                 g (f (inl x))   ＝⟨ η (inl x) ⟩
                 inl x           ∎)

  Ξ΅' : (y : Y) β†’ f' (g' y) ＝ y
  Ρ' y = inl-lc (inl (f' (g' y)) ＝⟨ (a (g' y))⁻¹ ⟩
                 f (inl (g' y))  ＝⟨ (ap f (b y))⁻¹ ⟩
                 f (g (inl y))   ＝⟨ Ρ (inl y) ⟩
                 inl y           ∎)

\end{code}

The old version from 21 March 2018, which uses function
extensionality:

\begin{code}

_βˆ–_ : (X : 𝓀 Μ‡ ) (a : X) β†’ 𝓀 Μ‡
X βˆ– a = Ξ£ x κž‰ X , x β‰  a

open import UF.FunExt

module _ (fe : FunExt) where

 open import UF.Base
 open import UF.Subsingletons-FunExt

 add-and-remove-point : {X : 𝓀 Μ‡ } β†’  X ≃ (X + πŸ™) βˆ– (inr ⋆)
 add-and-remove-point {𝓀} {X} = qinveq f (g , Ξ΅ , Ξ·)
  where
   f : X β†’ (X + πŸ™ {𝓀}) βˆ– inr ⋆
   f x = (inl x , +disjoint)

   g : (X + πŸ™) βˆ– inr ⋆ β†’ X
   g (inl x , u) = x
   g (inr ⋆ , u) = 𝟘-elim (u refl)

   η : f ∘ g ∼ id
   Ξ· (inl x , u) = to-Ξ£-＝' (negations-are-props (fe 𝓀 𝓀₀) _ _)
   Ξ· (inr ⋆ , u) = 𝟘-elim (u refl)

   Ρ : g ∘ f ∼ id
   Ξ΅ x = refl

 remove-points : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
               β†’ qinv f
               β†’ (a : X) β†’ X βˆ– a ≃ Y βˆ– (f a)
 remove-points {𝓀} {π“₯} {X} {Y} f (g , Ξ΅ , Ξ·) a = qinveq f' (g' , Ξ΅' , Ξ·')
  where
   f' : X βˆ– a β†’ Y βˆ– (f a)
   f' (x , u) = (f x , Ξ» (p : f x ＝ f a) β†’ u ((Ξ΅ x)⁻¹ βˆ™ ap g p βˆ™ Ξ΅ a))

   g' : Y βˆ– (f a) β†’ X βˆ– a
   g' (y , v) = (g y , Ξ» (p : g y ＝ a) β†’ v ((Ξ· y) ⁻¹ βˆ™ ap f p))

   Ρ' : g' ∘ f' ∼ id
   Ξ΅' (x , _) = to-Ξ£-＝ (Ξ΅ x , negations-are-props (fe 𝓀 𝓀₀) _ _)

   η' : f' ∘ g' ∼ id
   Ξ·' (y , _) = to-Ξ£-＝ (Ξ· y , negations-are-props (fe π“₯ 𝓀₀) _ _)

 add-one-and-remove-isolated-point : {Y : π“₯ Μ‡ } (z : Y + πŸ™)
                                   β†’ is-isolated z
                                   β†’ ((Y + πŸ™) βˆ– z) ≃ Y
 add-one-and-remove-isolated-point {π“₯} {Y} (inl b) i = qinveq f (g , Ξ΅ , Ξ·)
  where
   f : (Y + πŸ™) βˆ– (inl b) β†’ Y
   f (inl y , u) = y
   f (inr ⋆ , u) = b

   g' : (y : Y) β†’ is-decidable (inl b ＝ inl y) β†’ (Y + πŸ™) βˆ– (inl b)
   g' y (inl p) = (inr ⋆ , +disjoint')
   g' y (inr u) = (inl y , contrapositive (_⁻¹) u)

   g : Y β†’ (Y + πŸ™) βˆ– (inl b)
   g y = g' y (i (inl y))

   Ρ : g ∘ f ∼ id
   Ξ΅ (inl y , u) = to-Ξ£-＝ (p , negations-are-props (fe π“₯ 𝓀₀) _ _)
    where
     Ο† : (p : inl b ＝ inl y) (q : i (inl y) ＝ inl p) β†’ i (inl y) ＝ inr (β‰ -sym u)
     Ο† p q = 𝟘-elim (u (p ⁻¹))
     ψ : (v : inl b β‰  inl y) (q : i (inl y) ＝ inr v) β†’ i (inl y) ＝ inr (β‰ -sym u)
     ψ v q = q βˆ™ ap inr (negations-are-props (fe π“₯ 𝓀₀) _ _)
     h : i (inl y) ＝ inr (β‰ -sym u)
     h = equality-cases (i (inl y)) Ο† ψ
     p : pr₁ (g' y (i (inl y))) ＝ inl y
     p = ap (pr₁ ∘ (g' y)) h
   Ξ΅ (inr ⋆ , u) = equality-cases (i (inl b)) Ο† ψ
    where
     Ο† : (p : inl b ＝ inl b) β†’ i (inl b) ＝ inl p β†’ g (f (inr ⋆ , u)) ＝ (inr ⋆ , u)
     Ο† p q = r βˆ™ to-Ξ£-＝ (refl , negations-are-props (fe π“₯ 𝓀₀) _ _)
      where
       r : g b ＝ (inr ⋆ , +disjoint')
       r = ap (g' b) q
     ψ : (v : inl b β‰  inl b) β†’ i (inl b) ＝ inr v β†’ g (f (inr ⋆ , u)) ＝ (inr ⋆ , u)
     ψ v q = 𝟘-elim (v refl)

   η : f ∘ g ∼ id
   Ξ· y = equality-cases (i (inl y)) Ο† ψ
    where
     Ο† : (p : inl b ＝ inl y) β†’ i (inl y) ＝ inl p β†’ f (g' y (i (inl y))) ＝ y
     Ο† p q = ap (Ξ» - β†’ f (g' y -)) q βˆ™ inl-lc p
     ψ : (u : inl b β‰  inl y) β†’ i (inl y) ＝ inr u β†’ f (g' y (i (inl y))) ＝ y
     ψ _ = ap ((Ξ» d β†’ f (g' y d)))

 add-one-and-remove-isolated-point {π“₯} {Y} (inr ⋆) _ = ≃-sym add-and-remove-point

 +πŸ™-cancellable' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X + πŸ™) ≃ (Y + πŸ™) β†’ X ≃ Y
 +πŸ™-cancellable' {𝓀} {π“₯} {X} {Y} (Ο† , e) =
    X                  β‰ƒβŸ¨ add-and-remove-point ⟩
   (X + πŸ™) βˆ– inr ⋆     β‰ƒβŸ¨ remove-points Ο† (equivs-are-qinvs Ο† e) (inr ⋆) ⟩
   (Y + πŸ™) βˆ– Ο† (inr ⋆) β‰ƒβŸ¨ add-one-and-remove-isolated-point
                           (Ο† (inr ⋆))
                           (equivs-preserve-isolatedness Ο† e (inr ⋆)
                             new-point-is-isolated) ⟩
    Y                  β– 

\end{code}

Added 16th April 2021.

\begin{code}

open import UF.Subsingletons-FunExt

remove-and-add-isolated-point : funext 𝓀 𝓀₀
                              β†’ {X : 𝓀 Μ‡ } (xβ‚€ : X)
                              β†’ is-isolated xβ‚€
                              β†’ X ≃ (X βˆ– xβ‚€ + πŸ™ {π“₯})
remove-and-add-isolated-point fe {X} xβ‚€ ΞΉ = qinveq f (g , Ξ΅ , Ξ·)
 where
  Ο• : (x : X) β†’ is-decidable (xβ‚€ ＝ x) β†’ X βˆ– xβ‚€ + πŸ™
  Ο• x (inl p) = inr ⋆
  Ο• x (inr Ξ½) = inl (x , (Ξ» (p : x ＝ xβ‚€) β†’ Ξ½ (p ⁻¹)))

  f : X β†’ X βˆ– xβ‚€ + πŸ™
  f x = Ο• x (ΞΉ x)

  g : X βˆ– xβ‚€ + πŸ™ β†’ X
  g (inl (x , _)) = x
  g (inr ⋆) = xβ‚€

  Ξ·' : (y : X βˆ– xβ‚€ + πŸ™) (d : is-decidable (xβ‚€ ＝ g y)) β†’ Ο• (g y) d ＝ y
  η' (inl (x , ν)) (inl q) = 𝟘-elim (ν (q ⁻¹))
  Ξ·' (inl (x , Ξ½)) (inr _) = ap (Ξ» - β†’ inl (x , -)) (negations-are-props fe _ _)
  Ξ·' (inr ⋆) (inl p)       = refl
  Ξ·' (inr ⋆) (inr Ξ½)       = 𝟘-elim (Ξ½ refl)

  η : f ∘ g ∼ id
  Ξ· y = Ξ·' y (ΞΉ (g y))

  Ξ΅' : (x : X) (d : is-decidable (xβ‚€ ＝ x)) β†’ g (Ο• x d) ＝ x
  Ξ΅' x (inl p) = p
  Ξ΅' x (inr Ξ½) = refl

  Ρ : g ∘ f ∼ id
  Ξ΅ x = Ξ΅' x (ΞΉ x)

\end{code}