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}

Added 21st November 2022.

\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?