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:

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.

- 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?
- 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?
- 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--