Hi Nathan,

--

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 ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-= aa1cce32bcb2%40googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

-- I'm a bit rusty and don&=
#39;t want to say potentially misleading things on a public forum, so I'=
;m messaging offlist. Hopefully someone else gives more thorough answers:

=

1. ETT provides little (if any) technical value ove=
r set theory, at the cost of more bureaucracy, so it's main draw is the=
philosophical underpinnings. Since it also seems to conflict with computat=
ional intuitions, it alienates not only the classical mathematician, but al=
so the computer scientist--this leaves a small audience.

=

2. I believe you are correct

3. Without=
*any* type universes, you only get the types of System T---So you get a sy=
stem that corresponds to higher-typed Heyting arithmetic. So we need at lea=
st one universe. The HoTT book doesn't *really* use the natural numbers=
, only successor and a (binary) least upper bound operator. I guess this co=
rresponds roughly to Robinson's Arithmetic?

Be=
st,

Cory

On Thu, Jun 20, 2019 at 5:16 PM Nathan Carter <<=
a href=3D"mailto:nathancarter5@gmail.com">nathancarter5@gmail.com> w=
rote:

Hello, HoTT community.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 start wi= th a few small questions, and if anyone in the community here has time to a= nswer them, then I'll continue with others as needed.=C2=A0 Thank you i= n advance for any help you can give. (Where I'= m coming from:=C2=A0 I'm a mathematician; my dissertation was on interm= ediate logics, but I haven't focused on logic much for the past 15 year= s, instead doing mathematical software and some applied mathematics.=C2=A0 = I have a passion for clear exposition, so as I learn about HoTT, I process = 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 question.= =C2=A0 I'm bringing those questions here.)Her= e are three to start.

- Very early in the HoTT book, it tal= ks about the difference between types and sets, and says that HoTT encourag= es us to see sets as spaces.=C2=A0 Yet in a set of lecture videos Robert Ha= rper 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 In= tuitionistic Type Theory in a different direction than HoTT does, formalizi= ng the idea that types are sets.=C2=A0 Why does the HoTT book not mention t= his possibility?=C2=A0 Why does ETT not seem to get as much press as HoTT?<= /li>
- 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 are don= e more formally (twice, even).=C2=A0 The first of these two formalisms plac= es some restrictions on how one can introduce new judgmental equalities, wh= ich seem sufficient to guarantee its decidability, but at no point is an al= gorithm for deciding it given.=C2=A0 Is the algorithm simply to apply the o= nly applicable rule over and over to reduce each side, and then compare for= exact syntactic equality?
- One of my favorite things about HoTT as = a foundation for mathematics actually comes just from DTT:=C2=A0 Once you&#= 39;ve formalized pi types, you can define all of logic and (lots of) mathem= atics.=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 foundation= al level.=C2=A0 Am I right to be disappointed about that or am I missing so= mething?
Thanks in advance for any help you have time a= nd interest to provide!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 HomotopyTypeTheory+unsubscribe@googlegroups.com.

To view this discussion on the web visit ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-= aa1cce32bcb2%40googlegroups.com.

For more options, visit https://groups.google.com/d/optout.

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.com/d/msgid/HomotopyTypeTheory/CADzYOhd-tHN0XO_c%2B-rW_JSU= 1%3DQ6CmGE3L8aSHCEW32oX%2BKttA%40mail.gmail.com.

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

--0000000000001dda5b058bc3f746--