From: Michael Shulman <shulman@sandiego.edu> To: Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk> Cc: Nathan Carter <nathancarter5@gmail.com>, Homotopy Type Theory <homotopytypetheory@googlegroups.com> Subject: Re: [HoTT] my first 3 questions about HoTT Date: Thu, 20 Jun 2019 09:56:15 -0700 Message-ID: <CAOvivQzgvD8sqxbxn_2xOXQZ1XoSG4vnEe8LhcaQt_G2H8C6SQ@mail.gmail.com> (raw) In-Reply-To: <C02F9858-5868-4447-B0C1-D1303A754F60@exmail.nottingham.ac.uk> On Thu, Jun 20, 2019 at 9:39 AM Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk> wrote: >> Very early in the HoTT book, it talks about the difference between types and sets, and says that HoTT encourages us to see sets as spaces. Yet in a set of lecture videos Robert Harper did that I watched on YouTube (which also seem to have disappeared, so I cannot link to them here), he said that Extensional Type Theory takes Intuitionistic Type Theory in a different direction than HoTT does, formalizing the idea that types are sets. Why does the HoTT book not mention this possibility? Why does ETT not seem to get as much press as HoTT? > > ETT or computational type theory relies on some notion of untyped computation which is then sorted by defining some semantic criteria for types. I don't know what Harper was talking about in those lectures, but although he does often talk about computational type theory that assigns types to untyped computations, usually "Extensional Type Theory" refers not to that, but to an intrinsically typed theory like HoTT that contains a "reflection rule" saying that any two typally (nee "propositionally") equal terms are in fact judgmentally equal. In particular, this forces all types to be sets (i.e. 0-truncated). The HoTT book doesn't talk about this possibility because, well, it's a book about HoTT, not about ETT. ETT (with reflection rule) has an important disadvantage that its typechecking is no longer decidable. There have been some serious attempts to work with such type theories (e.g. http://www.andromeda-prover.org/), but there are also several other often-preferred approach if you want all types to be sets, such as assuming Uniqueness of Identity Proofs as an axiom (or an equivalent axiom such as Streicher's K), allowing unrestricted pattern-matching as in vanilla Agda, or fancier things like Observational Type Theory or the recent XTT (https://arxiv.org/abs/1904.08562). There's nothing wrong with these theories; they just serve a different purpose than HoTT. Indeed, such theories are sometimes combined with HoTT in a "two-level" type theory (e.g. https://arxiv.org/abs/1705.03307). > There is the remaining issue that it is not known whether the cubical theory coincides with the simplicial interpretation which is the standard one in homotopy theory. I would express the issue by saying that it's not yet known whether cubical type theory has all of (or even any of) the intended higher-categorical models. The simplicial interpretation is only one of these models. >> One of my favorite things about HoTT as a foundation for mathematics actually comes just from DTT: Once you've formalized pi types, you can define all of logic and (lots of) mathematics. But then the hierarchy of type universes seem to require that we understand the natural numbers, which is way more complicated than just pi types, and thus highly disappointing to have to bring in at a foundational level. Am I right to be disappointed about that or am I missing something? As Thorsten said, you won't get much of anywhere in mathematics without the natural numbers in your foundation. However, I suspect your disappointment has to do with the occurrence of natural numbers at "meta-level" to index the universe levels, rather than the natural numbers type that appears inside the theory. For comparison, note that ZFC has in fact countably infinitely many axioms, so it also involves some natural numbers at meta-level. However, it is nearly always possible to eliminate such meta-infinities by incorporating them into the object theory; for instance, ZFC can be replaced by the finitely axiomatizable NBG, and one can formulate type theories that "internalize" the universe levels. For instance, in Agda there is a *type* of "universe levels" over which the universes are parametrized. Our semantic understanding of such universe structures is currently fairly primitive, but I expect it will improve. -- 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/CAOvivQzgvD8sqxbxn_2xOXQZ1XoSG4vnEe8LhcaQt_G2H8C6SQ%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.

next prev parent reply indexThread overview:7+ messages / expand[flat|nested] mbox.gz Atom feed top 2019-06-20 16:16 Nathan Carter 2019-06-20 16:37 ` Cory Knapp 2019-06-20 16:39 ` Thorsten Altenkirch2019-06-20 16:56 ` Michael Shulman [this message]2019-06-20 23:11 ` Nathan Carter 2019-06-21 1:04 ` Michael Shulman 2019-06-20 16:48 ` Ali Caglayan

Reply instructions:You may reply publically 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-toswitches of git-send-email(1): git send-email \ --in-reply-to=CAOvivQzgvD8sqxbxn_2xOXQZ1XoSG4vnEe8LhcaQt_G2H8C6SQ@mail.gmail.com \ --to=shulman@sandiego.edu \ --cc=Thorsten.Altenkirch@nottingham.ac.uk \ --cc=homotopytypetheory@googlegroups.com \ --cc=nathancarter5@gmail.com \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting theIn-Reply-Toheader via mailto: links, try the mailto: link

Discussion of Homotopy Type Theory and Univalent Foundations Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott Newsgroup available over NNTP: nntp://inbox.vuxu.org/vuxu.archive.hott AGPL code for this site: git clone https://public-inbox.org/ public-inbox