```Discussion of Homotopy Type Theory and Univalent Foundations
help / color / mirror / Atom feed```
```From: Ali Caglayan <alizter@gmail.com>
To: Nathan Carter <nathancarter5@gmail.com>
Subject: Re: [HoTT] my first 3 questions about HoTT
Date: Thu, 20 Jun 2019 17:48:06 +0100	[thread overview]
Message-ID: <CAB17i=jRvovt+A7RWi2y5ocgV6H+KY5YX6bULWyrTQ0fuEYSxg@mail.gmail.com> (raw)

[-- Attachment #1: Type: text/plain, Size: 6979 bytes --]

1. There are at least two ways in which types are not sets. Firstly, when
reasoning classically, we have a membership relation whereby we can
postulate the membership of elements in a given set. It may seem similar to
a : A but in this case writing a : B would make no sense, whereas in set
theory membership can be disproven. This is quite a subtle notion and is
closely related to the difference between structural and material set
theories which Mike Shulman wrote a nice paper on
https://arxiv.org/pdf/1808.05204.pdf. But 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 Uniqueness of identity
proofs (UIP). This means that given a : A and b : A, we can form the
identity type Id(a, b). If we wish to show there is an equality between a
and b we construct a term p : Id(a, b). But what if we can construct
another equality q : Id(a, b)? UIP (a.k.a axiom K) ensures that there 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
construct 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 equal 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 "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.

2. One heuristic way to see that judgemental equality can be decided is by
"completely 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 fully
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. Universes
only need a sucessor structure, and not really the full arithmetic
capabilities of the natural numbers themselves.

These are just some of my thoughts on your questions, hopefully it will
help.

Ali Caglayan

On Thu, Jun 20, 2019 at 5:16 PM Nathan Carter <nathancarter5@gmail.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 answer on my own.  It
> was suggested that I ask them on this list.  I will start with a few small
> questions, and if anyone in the community here has time to answer them,
> then I'll continue with others as needed.  Thank you in advance for any
>
> (Where I'm coming from:  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.  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.
> When I can't explain something clearly, I flag it as a question.  I'm
> bringing those questions here.)
>
> Here are three to start.
>
>    1. Very early in the HoTT book, it talks about the difference between
>    types and sets, and says that HoTT encourages us to see sets as spaces.
>    Yet in a set of lecture videos Robert Harper 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 Intuitionistic Type Theory in a
>    different direction than HoTT does, formalizing the idea that types are
>    sets.  Why does the HoTT book not mention this possibility?  Why does ETT
>    not seem to get as much press as HoTT?
>    2. 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
>    suspected that perhaps the evidence was in Appendix A, where things are
>    done more formally (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 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 about HoTT as a foundation for
>    mathematics actually comes just from DTT:  Once you've formalized pi types,
>    you can define 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.  Am I right to
>    be disappointed about that or am I missing something?
>
>
> Nathan Carter
>
> --
> You received this message because you are subscribed to the Google Groups
> "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> To view this discussion on the web visit
> .
> For more options, visit https://groups.google.com/d/optout.
>

--
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB17i%3DjRvovt%2BA7RWi2y5ocgV6H%2BKY5YX6bULWyrTQ0fuEYSxg%40mail.gmail.com.

[-- Attachment #2: Type: text/html, Size: 8273 bytes --]
```

```     prev parent reply	other threads:[~2019-06-20 16:48 UTC|newest]

Thread overview: 7+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-06-20 16:16 Nathan Carter
2019-06-20 16:37 ` Cory Knapp
2019-06-20 16:39 ` Thorsten Altenkirch
2019-06-20 16:56   ` Michael Shulman
2019-06-20 23:11     ` Nathan Carter
2019-06-21  1:04       ` Michael Shulman
2019-06-20 16:48 ` Ali Caglayan [this message]
```

```Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,

Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

switches of git-send-email(1):

git send-email \
--to=alizter@gmail.com \
```This is a public inbox, see mirroring instructions