[HoTT] Type factorials

[HoTT] Type factorials

[Martín Hötzel Escardó]

[-- Attachment #1.1: Type: text/plain, Size: 3295 bytes --]

Probably just for amusement only.

(1) In the category of topological spaces (not up to homotopy), if X and Y 
are exponentiable and we topologize the space (X ≃ Y) of homeomorphisms of 
X and Y with the subspace topology, we get that

   co-derived-set (Y+1) × (X ≃ Y)  ≃  (X+1 ≃ Y+1).

The proof relies on classical logic.

Exponentiability is only needed to make sense of (X ≃ Y) as a space, and 
hence we could alternatively work with compactly generated spaces, which 
have all exponentials, but I haven't checked the above in that case (yet).

The derived set, in the sense of Cantor, is the set of limit points. Here 
we consider its complement, with the subspace topology, which of course is 
the discrete topology.

When X is the same space as Y, the above specializes to 

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

where Aut X is the space of auto (homeo)morphisms of X.

Hence when X is discrete, so that it is its own coderived set, the above 
specializes to the "factorial equation"

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

But if X is perfect in the sense of Cantor (has no isolated points), then 
instead we get 

 Aux X = Aut (X+1)

because the coderived set of X+1 is homeomorphic to 1.

(2) The above holds if we replace "space" by "homotopy type" and can be 
proved in HoTT/UF, *this time without appealing to classical logic* (and I 
doubt appealing to classical logic can simplify the argument, because the 
argument seems to be as simple and direct as it can be).

For this, we need the following definitions in HoTT/UF:

 * A point x is *isolated* if the type x=y is decidable for all y:X.
   (Counter-example: any point of the circle.)

 * A type is *discrete* if all its points are isolated.
   (Example: natural numbers, the finite type Fin n with n elements.)

 * A space is *perfect* if it has no isolated points.
   (Example: the circle.)

There is also a notion that doesn't arise above but that does arise in the 
proofs/constructions:

 * A point x is *h(omotopy)-isolated* if the type x=y is a proposition, 
   or a subsingleton, for every point y. 

   By local Hedberg, every isolated point is h-isolated.


(3) In particular, if Fin n is the type with n elements, 

    Fin (n+1) × Aut (Fin n)  ≃  Aut (Fin (n+1))

from which we get

    Fin (n!) ≃ Aut (Fin n)

by induction on n, as expected.

(4) Although the above development uses HoTT/UF ideas crucially, only 
function extensionality is needed to carry out the constructions and proofs 
(in particular, propositional extensionality and univalence are not needed).

I had fun formalizing the above ideas in Agda:

  https://www.cs.bham.ac.uk/~mhe/agda-new/UF-Factorial.html
  https://www.cs.bham.ac.uk/~mhe/agda-new/ArithmeticViaEquivalence.html

and so I wanted to share it here.

Best,
Martin


    

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/cb1c245d-987c-4da9-ac09-3814bfd096cf%40googlegroups.com.

[-- Attachment #1.2: Type: text/html, Size: 4449 bytes --]