[HoTT] Type factorialsurn:uuid:e2b4919c-a348-456f-7c70-2f40d59a7acf1970-01-01T00:00:01ZMartín Hötzel Escardóescardo.martin@gmail.com[HoTT] Type factorials1970-01-01T00:00:02Zurn:uuid:1ba73bc7-e0f7-d858-99b7-c00dd5c41bbf
```[-- 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

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.