Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: "Martín Hötzel Escardó" <escardo.martin@gmail.com>
To: Homotopy Type Theory <HomotopyTypeTheory@googlegroups.com>
Subject: [HoTT] Type factorials
Date: Thu, 28 Nov 2019 12:33:58 -0800 (PST)	[thread overview]
Message-ID: <cb1c245d-987c-4da9-ac09-3814bfd096cf@googlegroups.com> (raw)


[-- 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 --]

                 reply	other threads:[~2019-11-28 20:34 UTC|newest]

Thread overview: [no followups] expand[flat|nested]  mbox.gz  Atom feed

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=cb1c245d-987c-4da9-ac09-3814bfd096cf@googlegroups.com \
    --to=escardo.martin@gmail.com \
    --cc=HomotopyTypeTheory@googlegroups.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
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).