--
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 HomotopyTypeThe...@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.
Hi Nathan,
I can try to give answers but the answers you get may depend on the person you ask.
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.
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.
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
HomotopyTypeThe...@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.