```Discussion of Homotopy Type Theory and Univalent Foundations
help / color / mirror / Atom feed```
```* [HoTT] my first 3 questions about HoTT
@ 2019-06-20 16:16 Nathan Carter
2019-06-20 16:37 ` Cory Knapp
` (2 more replies)
0 siblings, 3 replies; 7+ messages in thread
From: Nathan Carter @ 2019-06-20 16:16 UTC (permalink / raw)
To: Homotopy Type Theory

[-- Attachment #1.1: Type: text/plain, Size: 3184 bytes --]

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
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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com.

[-- Attachment #1.2: Type: text/html, Size: 3666 bytes --]

```* Re: [HoTT] my first 3 questions about HoTT
2019-06-20 16:16 [HoTT] my first 3 questions about HoTT Nathan Carter
@ 2019-06-20 16:37 ` Cory Knapp
2019-06-20 16:39 ` Thorsten Altenkirch
2019-06-20 16:48 ` Ali Caglayan
2 siblings, 0 replies; 7+ messages in thread
From: Cory Knapp @ 2019-06-20 16:37 UTC (permalink / raw)
Cc: Homotopy Type Theory

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

Hi Nathan,

I'm a bit rusty and don't want to say potentially misleading things on a
public forum, so I'm messaging offlist. Hopefully someone else gives more

1. ETT provides little (if any) technical value over set theory, at the
cost of more bureaucracy, so it's main draw is the philosophical
underpinnings. Since it also seems to conflict with computational
intuitions, it alienates not only the classical mathematician, but also 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 system that corresponds to higher-typed Heyting arithmetic. So we
need at least one universe. The HoTT book doesn't *really* use the natural
numbers, only successor and a (binary) least upper bound operator. I guess
this corresponds roughly to Robinson's Arithmetic?

Best,
Cory

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.

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

```* Re: [HoTT] my first 3 questions about HoTT
2019-06-20 16:16 [HoTT] my first 3 questions about HoTT 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 16:48 ` Ali Caglayan
From: Thorsten Altenkirch @ 2019-06-20 16:39 UTC (permalink / raw)
To: Nathan Carter, Homotopy Type Theory

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

Hi Nathan,

I can try to give answers but the answers you get may depend on the person you ask.

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?
ETT or computational type theory relies on some notion of untyped computation which is then sorted by defining some semantic criteria for types. I prefer only to to talk about typed entities because they are the constructions which make sense and it shouldn’t be necessary to refer to some untyped codes. However, this is my preference, I am sure Bob Harper views this differently. Also the semantic definitions refer to a rather unspecified meta theory, while in a type theory specified as the initial syntax of some kind of algebras you get a precise and 1st order definition what exactly the theory and the models are.

1.  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?
It is beyond the scope of the HoTT book to discuss the algorithm to decide definitional equality. There are a number of standard approaches to do this: you can normalize the terms in a syntactic way and use this to decide equality but then you need to prove that the normalisation procedure actually terminates and is well behaved wrt typing which isn’t trivial. Another approach is to use a constructive semantical model to normalize (this is called normalisation by evaluation) but again this isn’t completely trivial. The naïve algorithm you suggest may not take care of eta-equalities.
Moreover, the theory presented in the HoTT book has a serious problem: extensionality principles like functional extensionality and univalence are added as axioms, which have no place in type theory. Their presence destroys computational adequacy, which means that a closed term of type Nat may not reduce to a numeral. Baiscally it is a programming language but we don’t know how to run the programs. This has been fixed now, by the work by Thierry Ciquand and others on cubical type theory, which uses the cubical sets interpretation of HoTT to give a constrictive semantics which in turn can be used to design a normalisation procedure which does normalize correctly, in particular it reduces closed natural numbers to numerals.
There is the remaining issue that it is not known whether the cubical theory coincides with the simplicial interpretation which is the standard one in homotopy theory.

1.  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?
How do you do a lot of Mathematics without defining the natural numbers? The problem with the predicative hierarchy of universes is rather that it is rather clumsy in real life since everything you do is usually level polymorphic. You can sort of put this under the carpet but actual implementations of type theory haven’t yet found a good way to deal with this.
Another issue with universes is that you always want more (they are like inaccessible cardinals in set theory). So for example you want to add a superuniverse which is above all the universes in the predicative hierarchy and so on. There has been some work investigating these universe hierarchies and the similarity with inaccessible cardinals is rather strong.
Thorsten

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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com<mailto:HomotopyTypeTheory+unsubscribe@googlegroups.com>.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
attachment.

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where permitted by law.

--
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/C02F9858-5868-4447-B0C1-D1303A754F60%40exmail.nottingham.ac.uk.

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

```* Re: [HoTT] my first 3 questions about HoTT
2019-06-20 16:16 [HoTT] my first 3 questions about HoTT Nathan Carter
2019-06-20 16:37 ` Cory Knapp
2019-06-20 16:39 ` Thorsten Altenkirch
@ 2019-06-20 16:48 ` Ali Caglayan
2 siblings, 0 replies; 7+ messages in thread
From: Ali Caglayan @ 2019-06-20 16:48 UTC (permalink / raw)
To: Nathan Carter; +Cc: Homotopy Type Theory

[-- 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 --]

```* Re: [HoTT] my first 3 questions about HoTT
2019-06-20 16:39 ` Thorsten Altenkirch
@ 2019-06-20 16:56   ` Michael Shulman
2019-06-20 23:11     ` Nathan Carter
From: Michael Shulman @ 2019-06-20 16:56 UTC (permalink / raw)
To: Thorsten Altenkirch; +Cc: Nathan Carter, Homotopy Type Theory

On Thu, Jun 20, 2019 at 9:39 AM Thorsten Altenkirch
<Thorsten.Altenkirch@nottingham.ac.uk> wrote:
>> 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?
>
> ETT or computational type theory relies on some notion of untyped computation which is then sorted by defining some semantic criteria for types.

I don't know what Harper was talking about in those lectures, but
although he does often talk about computational type theory that
assigns types to untyped computations, usually "Extensional Type
Theory" refers not to that, but to an intrinsically typed theory like
HoTT that contains a "reflection rule" saying that any two typally
(nee "propositionally") equal terms are in fact judgmentally equal.
In particular, this forces all types to be sets (i.e. 0-truncated).

ETT (with reflection rule) has an important disadvantage that its
typechecking is no longer decidable.  There have been some serious
attempts to work with such type theories (e.g.
http://www.andromeda-prover.org/), but there are also several other
often-preferred approach if you want all types to be sets, such as
assuming Uniqueness of Identity Proofs as an axiom (or an equivalent
axiom such as Streicher's K), allowing unrestricted pattern-matching
as in vanilla Agda, or fancier things like Observational Type Theory
or the recent XTT (https://arxiv.org/abs/1904.08562).  There's nothing
wrong with these theories; they just serve a different purpose than
HoTT.  Indeed, such theories are sometimes combined with HoTT in a
"two-level" type theory (e.g. https://arxiv.org/abs/1705.03307).

> There is the remaining issue that it is not known whether the cubical theory coincides with the simplicial interpretation which is the standard one in homotopy theory.

I would express the issue by saying that it's not yet known whether
cubical type theory has all of (or even any of) the intended
higher-categorical models.  The simplicial interpretation is only one
of these models.

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

As Thorsten said, you won't get much of anywhere in mathematics
without the natural numbers in your foundation.  However, I suspect
your disappointment has to do with the occurrence of natural numbers
at "meta-level" to index the universe levels, rather than the natural
numbers type that appears inside the theory.  For comparison, note
that ZFC has in fact countably infinitely many axioms, so it also
involves some natural numbers at meta-level.  However, it is nearly
always possible to eliminate such meta-infinities by incorporating
them into the object theory; for instance, ZFC can be replaced by the
finitely axiomatizable NBG, and one can formulate type theories that
"internalize" the universe levels.  For instance, in Agda there is a
*type* of "universe levels" over which the universes are parametrized.
Our semantic understanding of such universe structures is currently
fairly primitive, but I expect it will improve.

--
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/CAOvivQzgvD8sqxbxn_2xOXQZ1XoSG4vnEe8LhcaQt_G2H8C6SQ%40mail.gmail.com.

```* Re: [HoTT] my first 3 questions about HoTT
2019-06-20 16:56   ` Michael Shulman
@ 2019-06-20 23:11     ` Nathan Carter
2019-06-21  1:04       ` Michael Shulman
From: Nathan Carter @ 2019-06-20 23:11 UTC (permalink / raw)
To: Homotopy Type Theory

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

Thank you all (Thorsten, Ali, Michael, and some folks off-list, too) for the helpful responses.  I'll try to summarize here to be sure I've understood.  Please feel free to correct anything I say incorrectly.

1. Regarding ETT
People mentioned the loss of important computational properties if one adopts ETT, and I can certainly see why that would be a big deal.  While the subtleties relating 0-truncation, UIP, K, and reflection rules are not 100% clear to me, I at least have a high-level intuition, which is what I want at this point.

2. Decidability of judgmental equality
I got seemingly (to me?) conflicting answers.  One person off-list and one on-list said (I think) that applying all possible beta reductions and symbol definitions would be sufficient to decide judgmental equality; another said that this is not the case (again, I think).  But I was given a reference to a paper <https://link.springer.com/chapter/10.1007/978-3-540-70594-9_4>, so I can find out more on my own.

3. Numbers as universe indices
The responses showed that my question wasn't clear.  Saying something like "from pi types you can do all the things" was sloppy.  I was trying to express that, once you've defined pi types, you've (a) learned the rules about substitution, capture, etc., plus (b) encountered the principles by which types are defined in general (which I have other questions about...but later).  And from those two things, you can do lots of stuff.
Several folks said that "the natural numbers" is an overstatement, since successor and maximum are enough; responses suggested various things simpler than N that have these.
But Michael helped express my unease more precisely:  I'm not trying to do mathematics without the natural numbers; that would be silly and was part of my question's sloppiness.  Rather, I'm appreciating that DTT lets us build a foundation with fewer pieces than usual (cleaner than a dozen-or-so rules of ND with guards on variables appearing free in undischarged assumptions and so on, plus mathematical axioms).  To need a number system very early on seemed to lose some of this purity, especially since it seemed to be in the metatheory.  I do not (yet) fully understand Michael's answer about Agda's type of universe levels, but I guess that it avoids paradoxes by being one step removed from a type of all universes, which sounds clever.

These replies will help me make progress on my notes, so thank you very much again.  Once I've gotten to a good point for asking more questions, I will do so.

Nathan

--
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/6682FD3B-6A4C-49B4-B54D-E78FB4E71046%40gmail.com.

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

```* Re: [HoTT] my first 3 questions about HoTT
2019-06-20 23:11     ` Nathan Carter
@ 2019-06-21  1:04       ` Michael Shulman
0 siblings, 0 replies; 7+ messages in thread
From: Michael Shulman @ 2019-06-21  1:04 UTC (permalink / raw)
To: Nathan Carter; +Cc: Homotopy Type Theory

I think the reason for the mixed messages re: #2 is that different
type theories have different rules for judgmental equality.  If the
only rules for judgmental equality are "directed" ones like
beta-reduction, then (assuming a normalization result) to check
equality it generally suffices to reduce two terms to normal form and
compare the normal forms.  But if there are also other rules for
judgmental equality, like eta-conversion, that are difficult to
formulate in a "directed" way, then you generally need a fancier
equality-checking algorithm.  And some rules for judgmental equality,
like equality reflection in ETT, prevent there from being any
algorithm at all.

The HoTT Book assumes eta-conversion, so simple reduction to normal
forms is probably not sufficient.  There are well-understood
algorithms for equality-checking in MLTT with eta (generally built on
ideas like https://ncatlab.org/nlab/show/bidirectional+typechecking);
but Book HoTT also adds judgmental computation rules for
point-constructors of HITs, and while it seems intuitive that those
should be regarded as beta-reduction-like, I'm not aware that anyone
has precisely formulated an equality-checking algorithm for Book HoTT.

On Thu, Jun 20, 2019 at 4:11 PM Nathan Carter <nathancarter5@gmail.com> wrote:
>
>
> Thank you all (Thorsten, Ali, Michael, and some folks off-list, too) for the helpful responses.  I'll try to summarize here to be sure I've understood.  Please feel free to correct anything I say incorrectly.
>
> 1. Regarding ETT
> People mentioned the loss of important computational properties if one adopts ETT, and I can certainly see why that would be a big deal.  While the subtleties relating 0-truncation, UIP, K, and reflection rules are not 100% clear to me, I at least have a high-level intuition, which is what I want at this point.
>
> 2. Decidability of judgmental equality
> I got seemingly (to me?) conflicting answers.  One person off-list and one on-list said (I think) that applying all possible beta reductions and symbol definitions would be sufficient to decide judgmental equality; another said that this is not the case (again, I think).  But I was given a reference to a paper, so I can find out more on my own.
>
> 3. Numbers as universe indices
> The responses showed that my question wasn't clear.  Saying something like "from pi types you can do all the things" was sloppy.  I was trying to express that, once you've defined pi types, you've (a) learned the rules about substitution, capture, etc., plus (b) encountered the principles by which types are defined in general (which I have other questions about...but later).  And from those two things, you can do lots of stuff.
> Several folks said that "the natural numbers" is an overstatement, since successor and maximum are enough; responses suggested various things simpler than N that have these.
> But Michael helped express my unease more precisely:  I'm not trying to do mathematics without the natural numbers; that would be silly and was part of my question's sloppiness.  Rather, I'm appreciating that DTT lets us build a foundation with fewer pieces than usual (cleaner than a dozen-or-so rules of ND with guards on variables appearing free in undischarged assumptions and so on, plus mathematical axioms).  To need a number system very early on seemed to lose some of this purity, especially since it seemed to be in the metatheory.  I do not (yet) fully understand Michael's answer about Agda's type of universe levels, but I guess that it avoids paradoxes by being one step removed from a type of all universes, which sounds clever.
>
> These replies will help me make progress on my notes, so thank you very much again.  Once I've gotten to a good point for asking more questions, I will do so.
>
> Nathan
>
> --
> 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/6682FD3B-6A4C-49B4-B54D-E78FB4E71046%40gmail.com.
> 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/CAOvivQzbSbOCFrBK_X2-45eBovJ5e799wXrQPec9h1-sZUGH5Q%40mail.gmail.com.

```end of thread, other threads:[~2019-06-21  1:05 UTC | newest]

```This is a public inbox, see mirroring instructions