1. There are at least two ways in which types are not= sets. Firstly, when reasoning classically, we have a membership relation w= hereby we can postulate the membership of elements in a given set. It may s= eem similar to a : A but in this case writing a : B would make no sense, wh= ereas in set theory membership can be disproven. This is quite a subtle not= ion and is closely related to the difference between structural and materia= l set theories which Mike Shulman wrote a nice paper on=C2=A0https://arxiv.org/pdf/1808.05204.pdf= .=C2=A0But I am sure someone else here will do a better job at explain that= .

The second difference is what I think Harper was= referring to, which is that sets are types which satisfy what is called Un= iqueness of identity proofs (UIP). This means that given a : A and b : A, w= e can form the identity type Id(a, b). If we wish to show there is an equal= ity between a and b we construct a term p : Id(a, b). But what if we can co= nstruct another equality q : Id(a, b)? UIP (a.k.a axiom K) ensures that the= re is always a term r : Id(p, q). Which in English means: Any two proofs of= equality between elements of a set are themselves equal.

Why does this matter? Well because in Martin-Lof type theory (with = univalent universes) (the type theory that HoTT is based on), you can const= ruct seperate proofs of the same thing. Take for example the type 2. It has= two terms 1_2 : 2 and 2_2 : 2. If we consider the ways in which 2 can be e= qual to itself, i.e. terms of Id(2, 2), we see that (with univalence) there= are two possible ways. The first is just reflexivity and the second is &qu= ot;an equality" which swaps 1_2 with 2_2. These are both proofs of Id(= 2, 2) but they are definitely not the same. And in fact can't be shown = to be the same without assuming UIP.=C2=A0
=C2=A0
2. One heu= ristic way to see that judgemental equality can be decided is by "comp= letely computing" a given term, i.e. beta reduce it all the way down. = Theorems such as Church-Rosser guarantee that the order of reductions does = not matter. There are more properties such as "canonicity" which = roughly state that fully reduced terms are identical. I am not an expert on= these properties however but there are many experts on this list.

=
Checking whether two terms are judgementally equal is a commonly= studied problem in type theory. There are ways to test equality without fu= lly reducing down such as the one detailed here:

3. Simply typed lambda calculus has "natural numbers" via the = Church-encoding. The key difference between this and regular arithmetic is = that you can't really define a function out of the type of such things.= Or in other words, there is no recursion principle for the natural numbers= . Adding such a rule would give you something like Godels system T. Univers= es only need a sucessor structure, and not really the full arithmetic capab= ilities of the natural numbers themselves.

These a= re just some of my thoughts on your questions, hopefully it will help.

Ali Caglayan

On Thu, Jun 20, 2019 at 5:16 PM Nath= an Carter <nathancarter5@gmai= l.com> wrote:

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 answe= r on my own.=C2=A0 It was suggested that I ask them on this list.=C2=A0 I w= ill start with a few small questions, and if anyone in the community here h= as time to answer them, then I'll continue with others as needed.=C2=A0= Thank you in advance for any help you can give.

(= Where I'm coming from:=C2=A0 I'm a mathematician; my dissertation w= as on intermediate logics, but I haven't focused on logic much for the = past 15 years, instead doing mathematical software and some applied mathema= tics.=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 clearl= y 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.)

Here are three to start.
1. Very early in the HoTT b= ook, it talks about the difference between types and sets, and says that Ho= TT encourages us to see sets as spaces.=C2=A0 Yet in a set of lecture video= s Robert Harper did that I watched on YouTube (which also seem to have disa= ppeared, so I cannot link to them here), he said that Extensional Type Theo= ry takes Intuitionistic Type Theory in a different direction than HoTT does= , formalizing the idea that types are sets.=C2=A0 Why does the HoTT book no= t mention this possibility?=C2=A0 Why does ETT not seem to get as much pres= s as HoTT?
2. When that same text introduces judgmental equality, it c= laims 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 thi= ngs are done more formally (twice, even).=C2=A0 The first of these two form= alisms places some restrictions on how one can introduce new judgmental equ= alities, which seem sufficient to guarantee its decidability, but at no poi= nt 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 = compare for exact syntactic equality?
3. One of my favorite things abo= ut HoTT 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 re= quire 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.=C2=A0 Am I right to be disappointed about that or am I= missing something?
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 &= 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/CAB17i%3DjRvovt%2BA7RWi2y5o= cgV6H%2BKY5YX6bULWyrTQ0fuEYSxg%40mail.gmail.com.
For more options, visit http= s://groups.google.com/d/optout.
--000000000000dca320058bc41c77--