Hello, HoTT community.

<= /div>

I've learned a bit about HoTT in bits of spare time over the =
past few years, and have come up with some questions I can't answer on =
my own.=C2=A0 It was suggested that I ask them on this list.=C2=A0 I will s=
tart with a few small questions, and if anyone in the community here has ti=
me to answer them, then I'll continue with others as needed.=C2=A0 Than=
k you in advance for any help you can give.

(Where=
I'm coming from:=C2=A0 I'm a mathematician; my dissertation was on=
intermediate logics, but I haven't focused on logic much for the past =
15 years, instead doing mathematical software and some applied mathematics.=
=C2=A0 I have a passion for clear exposition, so as I learn about HoTT, I p=
rocess it by writing detailed notes to myself, explaining it as clearly as =
I can.=C2=A0 When I can't explain something clearly, I flag it as a que=
stion.=C2=A0 I'm bringing those questions here.)

- Very early in the HoTT book, = it talks about the difference between types and sets, and says that HoTT en= courages us to see sets as spaces.=C2=A0 Yet in a set of lecture videos Rob= ert Harper did that I watched on YouTube (which also seem to have disappear= ed, so I cannot link to them here), he said that Extensional Type Theory ta= kes Intuitionistic Type Theory in a different direction than HoTT does, for= malizing the idea that types are sets.=C2=A0 Why does the HoTT book not men= tion this possibility?=C2=A0 Why does ETT not seem to get as much press as = HoTT?
- When that same text introduces judgmental equality, it claims= that it is a decidable relation.=C2=A0 It does not seem to prove this, and= so I suspected that perhaps the evidence was in Appendix A, where things a= re done more formally (twice, even).=C2=A0 The first of these two formalism= s places some restrictions on how one can introduce new judgmental equaliti= es, which seem sufficient to guarantee its decidability, but at no point is= an algorithm for deciding it given.=C2=A0 Is the algorithm simply to apply= the only applicable rule over and over to reduce each side, and then compa= re for exact syntactic equality?
- One of my favorite things about Ho= TT as a foundation for mathematics actually comes just from DTT:=C2=A0 Once= you've formalized pi types, you can define all of logic and (lots of) = mathematics.=C2=A0 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 foun= dational level.=C2=A0 Am I right to be disappointed about that or am I miss= ing something?

Thanks in advance for any help you have =
time and interest to provide!

Nathan Carter

<=
div>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.google.co= m/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googleg= roups.com.

For more options, visit http= s://groups.google.com/d/optout.

------=_Part_2265_237964951.1561047395850-- ------=_Part_2264_1191050770.1561047395850--