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

 http://www.cse.chalmers.se/~nad/listings/equality/Function-universe.html#[βŠ€βŠŽβ†”βŠ€βŠŽ]↔[βŠ€βŠŽΓ—β†”]

See also Coquand's

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

and our

 https://www.cs.bham.ac.uk/~mhe/agda-new/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ΒΉ.

\begin{code}

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

open import UF-FunExt

\end{code}

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

\begin{code}

module UF-Factorial (fe : FunExt) where

open import SpartanMLTT
open import Plus-Properties
open import DiscreteAndSeparated
open import Swap
open import UF-Base
open import UF-Retracts
open import UF-Equiv
open import UF-Subsingletons-FunExt
open import UF-EquivalenceExamples
open import UF-Embeddings
open import UF-Subsingletons
open import UF-Equiv-FunExt
open import UF-Miscelanea

\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-a-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-a-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-a-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-a-prop fe g _ i)

   Ξ΅ : Ο† ∘ Ξ³ ∼ id
   Ξ΅ ((f , i) , p) = to-Ξ£-≑
                      (to-subtype-≑ (being-equiv-is-a-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-a-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-a-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-a-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 + πŸ™) ( +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                          β‰ƒβŸ¨ ≃-sym (πŸ™-lneutral {universe-of X} {universe-of X})                               ⟩
  πŸ™ Γ— Aut X                      β‰ƒβŸ¨ Γ—cong (≃-sym (singleton-≃-πŸ™ (perfect-coderived-singleton X i))) (≃-refl (Aut X)) ⟩
  co-derived-set (X + πŸ™) Γ— Aut X β‰ƒβŸ¨ general-factorial X                                                              ⟩
  Aut (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-a-prop fe) (dfunext (fe _ _) (Ξ» y β†’ 𝟘-elim y))
  Ξ΅ : (x : πŸ™) β†’ g (f x) ≑ x
  Ξ΅ * = refl

\end{code}