Hi Nathan,

I can try to give answers but the answers you get ma= y depend on the person you ask.

1. Very early in the HoTT book, it talks about the difference between types an= d sets, and says that HoTT encourages us to see sets as spaces.  Yet i= n a set of lecture videos Robert Harper did that I watched on YouTube (whic= h also seem to have disappeared, so I cannot link to them here), he said that Extensional Type Theory takes Intu= itionistic Type Theory in a different direction than HoTT does, formalizing= the idea that types are sets.  Why does the HoTT book not mention thi= s 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 typ= es. I prefer only to to talk about typed entities because they are the constructions which make sense and it should= n=E2=80=99t be necessary to refer to some untyped codes. However, this is m= y preference, I am sure Bob Harper views this differently. Also the semanti= c definitions refer to a rather unspecified meta theory, while in a type theory specified as the initial syntax of som= e kind of algebras you get a precise and 1st order definition wh= at 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 suspecte= d that perhaps the evidence was in Appendix A, where things are done more f= ormally (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 algor= ithm simply to apply the only applicable rule over and over to reduce each side, and then compare for exact syntact= ic equality?

It is beyond the scope of the HoTT book to discuss the algorithm t= o decide definitional equality. There are a number of standard approaches t= o do this: you can normalize the terms in a syntactic way and use this to decide equality but then you need to pr= ove that the normalisation procedure actually terminates and is well behave= d wrt typing which isn=E2=80=99t trivial. Another approach is to use a cons= tructive semantical model to normalize (this is called normalisation by evaluation) but again this isn=E2=80=99t comple= tely trivial. The na=C3=AFve algorithm you suggest may not take care of eta= -equalities.

Moreover, the theory presented in the HoTT book has a serious prob= lem: extensionality principles like functional extensionality and univalenc= e are added as axioms, which have no place in type theory. Their presence destroys computational adequacy, whic= h means that a closed term of type Nat may not reduce to a numeral. Baiscal= ly it is a programming language but we don=E2=80=99t know how to run the pr= ograms. 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 normaliz= e correctly, in particular it reduces closed natural numbers to numerals.

There is the remaining issue that it is not known whether the cubi= cal theory coincides with the simplicial interpretation which is the standa= rd one in homotopy theory.

1. One of my favorite things about HoTT as a foundation for mathematics actual= ly comes just from DTT:  Once you've formalized pi types, you can defi= ne 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.&nbs= p; 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 nu= mbers? The problem with the predicative hierarchy of universes is rather th= at 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=E2=80= =99t yet found a good way to deal with this.

Another issue with universes is that you always want more (they ar= e like inaccessible cardinals in set theory). So for example you want to ad= d 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 inacc= essible cardinals is rather strong.

Thorsten

Nathan Carter

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to Homo= topyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://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
attachment.=20

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=20
where permitted by law.

```

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.go= ogle.com/d/msgid/HomotopyTypeTheory/C02F9858-5868-4447-B0C1-D1303A754F60%40= exmail.nottingham.ac.uk.
For more options, visit http= s://groups.google.com/d/optout.
--_000_C02F985858684447B0C1D1303A754F60exmailnottinghamacuk_--