Hi Nathan,
I can try to give answers but the answers you get may depend on the person you ask.
1. 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 prefer only to to talk about typed entities because they are the constructions which make sense and it shouldn’t be necessary to refer to some untyped codes. However, this is my preference, I am sure Bob Harper views this differently. Also the semantic definitions refer to a rather unspecified meta theory, while in a type theory specified as the initial syntax of some kind of algebras you get a precise and 1st order definition what exactly the theory and the models are.
1. When that same text introduces judgmental equality, it claims that it is a decidable relation. It does not seem to prove this, and so I suspected that perhaps the evidence was in Appendix A, where things are done more formally (twice, even). The first of these two formalisms places some restrictions on how one can introduce new judgmental equalities, which seem sufficient to guarantee its decidability, but at no point is an algorithm for deciding it given. Is the algorithm simply to apply the only applicable rule over and over to reduce each side, and then compare for exact syntactic equality?
It is beyond the scope of the HoTT book to discuss the algorithm to decide definitional equality. There are a number of standard approaches to do this: you can normalize the terms in a syntactic way and use this to decide equality but then you need to prove that the normalisation procedure actually terminates and is well behaved wrt typing which isn’t trivial. Another approach is to use a constructive semantical model to normalize (this is called normalisation by evaluation) but again this isn’t completely trivial. The naïve algorithm you suggest may not take care of eta-equalities.
Moreover, the theory presented in the HoTT book has a serious problem: extensionality principles like functional extensionality and univalence are added as axioms, which have no place in type theory. Their presence destroys computational adequacy, which means that a closed term of type Nat may not reduce to a numeral. Baiscally it is a programming language but we don’t know how to run the programs. This has been fixed now, by the work by Thierry Ciquand and others on cubical type theory, which uses the cubical sets interpretation of HoTT to give a constrictive semantics which in turn can be used to design a normalisation procedure which does normalize correctly, in particular it reduces closed natural numbers to numerals.
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.
1. 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?
How do you do a lot of Mathematics without defining the natural numbers? The problem with the predicative hierarchy of universes is rather that it is rather clumsy in real life since everything you do is usually level polymorphic. You can sort of put this under the carpet but actual implementations of type theory haven’t yet found a good way to deal with this.
Another issue with universes is that you always want more (they are like inaccessible cardinals in set theory). So for example you want to add a superuniverse which is above all the universes in the predicative hierarchy and so on. There has been some work investigating these universe hierarchies and the similarity with inaccessible cardinals is rather strong.
Thorsten
Thanks in advance for any help you have time and interest to provide!
Nathan Carter
--
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/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.
--
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/C02F9858-5868-4447-B0C1-D1303A754F60%40exmail.nottingham.ac.uk.
For more options, visit https://groups.google.com/d/optout.