From: Michael Shulman <firstname.lastname@example.org>
To: Thorsten Altenkirch <Thorsten.Altenkirch@nottingham.ac.uk>
Cc: Nathan Carter <email@example.com>,
Homotopy Type Theory <firstname.lastname@example.org>
Subject: Re: [HoTT] my first 3 questions about HoTT
Date: Thu, 20 Jun 2019 09:56:15 -0700 [thread overview]
Message-ID: <CAOvivQzgvD8sqxbxn_2xOXQZ1XoSG4vnEe8LhcaQt_G2H8C6SQ@mail.gmail.com> (raw)
On Thu, Jun 20, 2019 at 9:39 AM Thorsten Altenkirch
>> 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 HomotopyTypeTheoryemail@example.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 other threads:[~2019-06-20 16:56 UTC|newest]
Thread 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 Altenkirch
2019-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
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:
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
* 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).