Martin Escardo, 2017, written in Agda November 2019.

If X is discrete then

(X + 𝟙) × Aut X ≃ Aut (X + 𝟙),

where

Aut X := (X ≃ X)

is the type of automorphisms of the type X.

This is proved by Danielsson in

https://github.com/simhu/cubical/blob/master/examples/finite.cub

and our

https://www.cs.bham.ac.uk/~mhe/TypeTopology/PlusOneLC.html

More generally, for an arbitraty type X, we prove that

co-derived-set (X + 𝟙) × Aut X ≃ Aut (X + 𝟙),

where the co-derived-set of a type is the subtype of isolated points.

In particular, if X is discrete (all its points are isolated), then we
get the "factorial equivalence"

(X + 𝟙) × Aut X ≃ Aut (X + 𝟙).

On the other hand, if X is perfect (has no isolated points), then

Aut X ≃ Aut (X + 𝟙),

This is the case, for example, if X is the circle S¹.

But if P is a proposition, then

P + 𝟙 ≃ Aut (P + 𝟙).

\begin{code}

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

open import UF.FunExt

\end{code}

We need functional extensionality (but not propositional
extensionality or univalence).

\begin{code}

module Factorial.Law (fe : FunExt) where

open import Factorial.Swap
open import MLTT.Plus-Properties
open import MLTT.Spartan
open import UF.Base
open import UF.DiscreteAndSeparated
open import UF.Embeddings
open import UF.Equiv
open import UF.Equiv-FunExt
open import UF.EquivalenceExamples
open import UF.Retracts
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

\end{code}

We refer to set of isolated points as the co derived set (for
complement of the derived set, in the sense of Cantor, consisting of
the limit points, i.e. non-isolated points).

Recall that a point x : X is isolated if the identity type x ＝ y is
decidable for every y : X.

\begin{code}

co-derived-set : 𝓤 ̇ → 𝓤 ̇
co-derived-set X = Σ x ꞉ X , is-isolated x

cods-embedding : (X : 𝓤 ̇ ) → co-derived-set X → X
cods-embedding X = pr₁

cods-embedding-is-embedding : (X : 𝓤 ̇ ) → is-embedding (cods-embedding X)
cods-embedding-is-embedding X = pr₁-is-embedding (being-isolated-is-prop fe)

cods-embedding-is-equiv : (X : 𝓤 ̇ ) → is-discrete X → is-equiv (cods-embedding X)
cods-embedding-is-equiv X d = pr₁-is-equiv X is-isolated
(λ x → pointed-props-are-singletons (d x)
(being-isolated-is-prop fe x))

≃-cods : (X : 𝓤 ̇ ) → is-discrete X → co-derived-set X ≃ X
≃-cods X d = cods-embedding X , cods-embedding-is-equiv X d

\end{code}

Exercise. Prove that the co derived set is a set in the sense of
univalent mathematics.

Recall that a type is perfect if it has no isolated points.

\begin{code}

perfect-coderived-empty : (X : 𝓤 ̇ ) → is-perfect X → is-empty (co-derived-set X)
perfect-coderived-empty X i (x , j) = i (x , j)

perfect-coderived-singleton : (X : 𝓤 ̇ ) → is-perfect X → is-singleton (co-derived-set (X + 𝟙 {𝓥}))
perfect-coderived-singleton X i = (inr ⋆ , new-point-is-isolated) , γ
where
γ : (c : co-derived-set (X + 𝟙)) → inr ⋆ , new-point-is-isolated ＝ c
γ (inl x , j) = 𝟘-elim (i (x , a))
where
a : is-isolated x
a = embeddings-reflect-isolatedness inl (inl-is-embedding X 𝟙) x j
γ (inr ⋆ , j) = to-Σ-＝' (being-isolated-is-prop fe (inr ⋆) new-point-is-isolated j)

\end{code}

For a type A, denote by A' the co-derived set of A.

Then we get a map

(Y+𝟙)' × (X ≃ Y) → (X+𝟙 ≃ Y+𝟙),

where the choice of isolated point a:Y+𝟙 controls which equivalence
X+𝟙≃Y+𝟙 we get from the equivalence f: X≃Y:

f+𝟙       swap (a , inr (⋆))
X+𝟙 ----> Y+𝟙 --------------------> Y+𝟙

The claim is that the above map is an equivalence.

We construct/prove this in four steps:

(1)  (X ≃ Y)
≃ Σ f ꞉ X + 𝟙 ≃ Y + 𝟙 , f (inr ⋆) ＝ inr ⋆

Hence

(2) (Y + 𝟙)' × (X ≃ Y)
≃ (Y + 𝟙)' × Σ f ꞉ X + 𝟙 ≃ Y + 𝟙 , f (inr ⋆) ＝ inr ⋆

Also

(3) (Y + 𝟙)' × (Σ f ꞉ X + 𝟙 ≃ Y + 𝟙 , f (inr ⋆) ＝ inr ⋆)
≃ (X + 𝟙 ≃ Y + 𝟙)

And therefore

(4) (Y + 𝟙)' × (X ≃ Y)
≃ (X + 𝟙 ≃ Y + 𝟙)

\end{code}

\begin{code}

module factorial-steps
{𝓤 𝓥 : Universe}
(𝓦 𝓣 : Universe)
(X : 𝓤 ̇ )
(Y : 𝓥 ̇ )
where

X+𝟙 = X + 𝟙 {𝓦}
Y+𝟙 = Y + 𝟙 {𝓣}

\end{code}

In the following, we use the fact that if f (inr ⋆) ＝ inr ⋆ for a
function, f : X+𝟙 → Y+𝟙, then f (inl x) is of the form inl y
(inl-preservation).

\begin{code}

lemma : (f : X+𝟙 → Y+𝟙)
→ f (inr ⋆) ＝ inr ⋆
→ is-equiv f
→ Σ f' ꞉ (X → Y), is-equiv f' × (f ∼ +functor f' unique-to-𝟙)
lemma f p i = γ (equivs-are-qinvs f i)
where
γ : qinv f → Σ f' ꞉ (X → Y), is-equiv f' × (f ∼ +functor f' unique-to-𝟙)
γ (g , η , ε) = f' , qinvs-are-equivs f' (g' , η' , ε') , h
where
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 (inr ⋆)     ＝⟨ (ap g p)⁻¹ ⟩
g (f (inr ⋆)) ＝⟨ η (inr ⋆) ⟩
inr ⋆         ∎

g' : Y → X
g' x = pr₁ (inl-preservation g q (sections-are-lc g (f , ε)) x)

b : (y : Y) → g (inl y) ＝ inl (g' y)
b y = pr₂ (inl-preservation g q (sections-are-lc g (f , ε)) y)

η' : g' ∘ f' ∼ id
η' 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           ∎)

ε' : f' ∘ g' ∼ id
ε' 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           ∎)

h : f ∼ +functor f' unique-to-𝟙
h (inl x) = a x
h (inr ⋆) = p

step₁ : (X ≃ Y) ≃ (Σ f ꞉ X+𝟙 ≃ Y+𝟙 , ⌜ f ⌝ (inr ⋆) ＝ inr ⋆)
step₁ = qinveq φ (γ , η , ε)
where
a : (g : X → Y) → qinv g → Y+𝟙 → X+𝟙
a g (g' , η , ε) = +functor g' unique-to-𝟙

b : (g : X → Y) (q : qinv g) → a g q ∘ +functor g unique-to-𝟙 ∼ id
b g (g' , η , ε) (inl x) = ap inl (η x)
b g (g' , η , ε) (inr ⋆) = refl

c : (g : X → Y) (q : qinv g) → +functor g unique-to-𝟙 ∘ a g q ∼ id
c g (g' , η , ε) (inl y) = ap inl (ε y)
c g (g' , η , ε) (inr ⋆) = refl

d : (g : X → Y) → qinv g → is-equiv (+functor g unique-to-𝟙)
d g q = qinvs-are-equivs (+functor g unique-to-𝟙) (a g q , b g q , c g q)

φ : (X ≃ Y) → Σ e ꞉ X+𝟙 ≃ Y+𝟙 , ⌜ e ⌝ (inr ⋆) ＝ inr ⋆
φ (g , i) = (+functor g unique-to-𝟙 , d g (equivs-are-qinvs g i)) , refl

γ : (Σ e ꞉ X+𝟙 ≃ Y+𝟙 , ⌜ e ⌝ (inr ⋆) ＝ inr ⋆) → (X ≃ Y)
γ ((f , i) , p) = pr₁ (lemma f p i) , pr₁ (pr₂ (lemma f p i))

η : γ ∘ φ ∼ id
η (g , i) = to-Σ-＝ (refl , being-equiv-is-prop fe g _ i)

ε : φ ∘ γ ∼ id
ε ((f , i) , p) = to-Σ-＝
(to-subtype-＝ (being-equiv-is-prop fe) r ,
isolated-is-h-isolated (f (inr ⋆))
(equivs-preserve-isolatedness f i (inr ⋆) new-point-is-isolated) _ p)
where
s : f ∼ pr₁ (pr₁ ((φ ∘ γ) ((f , i) , p)))
s (inl x) = pr₂ (pr₂ (lemma f p i)) (inl x)
s (inr ⋆) = p

r : pr₁ (pr₁ ((φ ∘ γ) ((f , i) , p))) ＝ f
r = dfunext (fe _ _) (λ z → (s z)⁻¹)

step₂ : co-derived-set (Y+𝟙) × (X ≃ Y)
≃ co-derived-set (Y+𝟙) × (Σ e ꞉ X+𝟙 ≃ Y+𝟙 , ⌜ e ⌝ (inr ⋆) ＝ inr ⋆)
step₂ = ×-cong (≃-refl (co-derived-set (Y+𝟙))) step₁

step₃ : (co-derived-set (Y+𝟙) × (Σ e ꞉ X+𝟙 ≃ Y+𝟙 , ⌜ e ⌝ (inr ⋆) ＝ inr ⋆))
≃ (X+𝟙 ≃ Y+𝟙)
step₃ = qinveq φ (γ , η , ε)
where
A = co-derived-set (Y+𝟙) × (Σ e ꞉ X+𝟙 ≃ Y+𝟙 , ⌜ e ⌝ (inr ⋆) ＝ inr ⋆)
B = X+𝟙 ≃ Y+𝟙

φ : A → B
φ ((t , i) , ((f , j) , p)) = g , k
where
g : X+𝟙 → Y+𝟙
g = swap t (inr ⋆) i new-point-is-isolated ∘ f

k : is-equiv g
k = ∘-is-equiv-abstract j (swap-is-equiv t (inr ⋆) i new-point-is-isolated)

γ : B → A
γ (g , k) = (t , i) , ((f , j) , p)
where
t : Y+𝟙
t = g (inr ⋆)

i : is-isolated t
i = equivs-preserve-isolatedness g k (inr ⋆) new-point-is-isolated

f : X+𝟙 → Y+𝟙
f = swap t (inr ⋆) i new-point-is-isolated ∘ g

j : is-equiv f
j = ∘-is-equiv-abstract k (swap-is-equiv t (inr ⋆) i new-point-is-isolated)

p : f (inr ⋆) ＝ inr ⋆
p = swap-equation₀ t (inr ⋆) i new-point-is-isolated

η : γ ∘ φ ∼ id
η ((t , i) , ((f , j) , p)) = s
where
g : X+𝟙 → Y+𝟙
g = swap t (inr ⋆) i new-point-is-isolated ∘ f

k : is-equiv g
k = ∘-is-equiv-abstract j (swap-is-equiv t (inr ⋆) i new-point-is-isolated)

t' : Y+𝟙
t' = g (inr ⋆)

i' : is-isolated t'
i' = equivs-preserve-isolatedness g k (inr ⋆) new-point-is-isolated

q : t' ＝ t
q = g (inr ⋆)                                      ＝⟨ a ⟩
swap t (inr ⋆) i new-point-is-isolated (inr ⋆) ＝⟨ b ⟩
t                                              ∎
where
a = ap (swap t (inr ⋆) i new-point-is-isolated) p
b = swap-equation₁ t (inr ⋆) i new-point-is-isolated

r : (t' , i') ＝ (t , i)
r = to-subtype-＝ (being-isolated-is-prop fe) q

f' : X+𝟙 → Y+𝟙
f' = swap t' (inr ⋆) i' new-point-is-isolated ∘ g

j' : is-equiv f'
j' = ∘-is-equiv-abstract k (swap-is-equiv t' (inr ⋆) i' new-point-is-isolated)

h : f' ∼ f
h z = swap t' (inr ⋆) i' new-point-is-isolated
(swap t (inr ⋆) i new-point-is-isolated (f z))    ＝⟨ a ⟩

swap t (inr ⋆) i new-point-is-isolated
(swap t (inr ⋆) i new-point-is-isolated (f z))    ＝⟨ b ⟩

f z                                                ∎
where
ψ : co-derived-set (Y+𝟙) → Y+𝟙
ψ (t' , i') = swap t' (inr ⋆) i' new-point-is-isolated
(swap t (inr ⋆) i new-point-is-isolated (f z))
a = ap ψ r
b = swap-involutive t (inr ⋆) i new-point-is-isolated (f z)

m : is-isolated (f (inr ⋆))
m = equivs-preserve-isolatedness f j (inr ⋆) new-point-is-isolated

n : {t : Y+𝟙} → is-prop (f (inr ⋆) ＝ t)
n = isolated-is-h-isolated (f (inr ⋆)) m

o : f' , j' ＝ f , j
o = to-subtype-＝ (being-equiv-is-prop fe) (dfunext (fe _ _) h)

p' : f' (inr ⋆) ＝ inr ⋆
p' = swap-equation₀ t' (inr ⋆) i' new-point-is-isolated

s : ((t' , i') , ((f' , j') , p')) ＝ ((t , i) , ((f , j) , p))
s = to-×-＝ r (to-Σ-＝ (o , n top' p))
where
top' = transport (λ - → ⌜ - ⌝ (inr ⋆) ＝ inr ⋆) o p'

ε : φ ∘ γ ∼ id
ε (g , k) = r
where
z : Y+𝟙
z = g (inr ⋆)

i : is-isolated z
i = equivs-preserve-isolatedness g k (inr ⋆) new-point-is-isolated

h : (swap (g (inr ⋆)) (inr ⋆) i new-point-is-isolated)
∘ (swap (g (inr ⋆)) (inr ⋆) i new-point-is-isolated)
∘ g
∼ g
h = swap-involutive z (inr ⋆) i new-point-is-isolated ∘ g

r : φ (γ (g , k)) ＝ (g , k)
r = to-Σ-＝ (dfunext (fe _ _) h , being-equiv-is-prop fe g _ k)

step₄ : co-derived-set (Y+𝟙) × (X ≃ Y) ≃ (X+𝟙 ≃ Y+𝟙)
step₄ = step₂ ● step₃

\end{code}

This is the end of the submodule, which has the following corollaries:

\begin{code}

general-factorial : (X : 𝓤 ̇ ) → co-derived-set (X + 𝟙) × Aut X ≃ Aut (X + 𝟙)
general-factorial {𝓤} X = factorial-steps.step₄ 𝓤 𝓤 X X

discrete-factorial : (X : 𝓤 ̇ )
→ is-discrete X
→ (X + 𝟙) × Aut X ≃ Aut (X + 𝟙)
discrete-factorial X d = γ
where
i = ×-cong (≃-sym (≃-cods (X + 𝟙) ( +-is-discrete d 𝟙-is-discrete))) (≃-refl (Aut X))

γ = (X + 𝟙) × Aut X                ≃⟨ i ⟩
co-derived-set (X + 𝟙) × Aut X ≃⟨ general-factorial X ⟩
Aut (X + 𝟙)                    ■

perfect-factorial : (X : 𝓤 ̇ )
→ is-perfect X
→ Aut X ≃ Aut (X + 𝟙)
perfect-factorial {𝓤} X i =
Aut X                          ≃⟨ I ⟩
𝟙 × Aut X                      ≃⟨ II ⟩
co-derived-set (X + 𝟙) × Aut X ≃⟨ III ⟩
Aut (X + 𝟙)                    ■
where
I   =  ≃-sym (𝟙-lneutral {𝓤} {𝓤})
II  = ×-cong (≃-sym (singleton-≃-𝟙 (perfect-coderived-singleton X i))) (≃-refl (Aut X))
III = general-factorial X

\end{code}

Exercise. Conclude that the map (-)+𝟙 : 𝓤 ̇ → 𝓤 ̇, although it is
left-cancellable, is not an embedding, but that it is an embedding
when restricted to perfect types.

We should not forget the (trivial) "base case":

\begin{code}

factorial-base : 𝟙 {𝓥} ≃ Aut (𝟘 {𝓤})
factorial-base = f , ((g , η) , (g , ε))
where
f : 𝟙 → Aut 𝟘
f _ = id , ((id , (λ _ → refl)) , (id , (λ _ → refl)))

g : Aut 𝟘 → 𝟙
g = unique-to-𝟙

η : (e : Aut 𝟘) → f (g e) ＝ e
η _ = to-subtype-＝ (being-equiv-is-prop fe) (dfunext (fe _ _) (λ y → 𝟘-elim y))

ε : (x : 𝟙) → g (f x) ＝ x
ε ⋆ = refl

\end{code}

\begin{code}

Aut-of-prop-is-singleton : (P : 𝓤 ̇ )
→ is-prop P
→ is-singleton (Aut P)
Aut-of-prop-is-singleton P i = ≃-refl P , h
where
h : (e : P ≃ P) → ≃-refl P ＝ e
h (f , _) = to-subtype-＝
(being-equiv-is-prop fe)
(dfunext (fe _ _) (λ p → i p (f p)))

factorial-base-generalized : (P : 𝓤 ̇ )
→ is-prop P
→ 𝟙 {𝓥} ≃ Aut P
factorial-base-generalized P i = singleton-≃-𝟙' (Aut-of-prop-is-singleton P i)

propositional-factorial : (P : 𝓤 ̇ )
→ is-prop P
→ (P + 𝟙) ≃ Aut (P + 𝟙)
propositional-factorial {𝓤} P i =
P + 𝟙             ≃⟨ I ⟩
(P + 𝟙) × (𝟙 {𝓤}) ≃⟨ II ⟩
(P + 𝟙) × Aut P   ≃⟨ III ⟩
Aut (P + 𝟙)       ■
where
I   = ≃-sym 𝟙-rneutral
II  = ×-cong (≃-refl (P + 𝟙)) (factorial-base-generalized P i)
III = discrete-factorial P (props-are-discrete i)

\end{code}

Is the converse also true?