my first 3 questions about HoTT

[Nathan Carter]

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 help you can give.

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

Thanks in advance for any help you have time and interest to provide!

Nathan Carter

[Cory Knapp]

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 thorough answers:

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

--
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 HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Thorsten Altenkirch]

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 1^st order definition what exactly the theory and the models are.

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?

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.

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?

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

 

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 "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/d62ccb9e-10d7-4884-bb09-aa1cce32bcb2%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
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.

[Ali Caglayan]

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:

https://link.springer.com/chapter/10.1007/978-3-540-70594-9_4

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 <nathan...@gmail.com> wrote:

[Michael Shulman]

On Thu, Jun 20, 2019 at 9:39 AM Thorsten Altenkirch
<Thorsten....@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).

The HoTT book doesn't talk about this possibility because, well, it's
a book about HoTT, not about ETT.

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.

[Nathan Carter]

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

[Michael Shulman]

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.

> --
> 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 HomotopyTypeThe...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/6682FD3B-6A4C-49B4-B54D-E78FB4E71046%40gmail.com.