* [HoTT] Type factorials
@ 2019-11-28 20:33 Martín Hötzel Escardó
0 siblings, 0 replies; only message in thread
From: Martín Hötzel Escardó @ 2019-11-28 20:33 UTC (permalink / raw)
To: Homotopy Type Theory
[-- 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
* 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:
and so I wanted to share it here.
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 HomotopyTypeTheoryemail@example.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 --]
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2019-11-28 20:34 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-11-28 20:33 [HoTT] Type factorials Martín Hötzel Escardó
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).