It's worth mentioning that the situation with "the axiom of choice for all types" is a bit more complicated than that. It's true that one obvious statement which might go by that name, namely "every surjection has a section", is inconsistent with univalence. However, there are other versions of AC that say something about types of arbitrary level but are consistent with univalence. For instance, there is the traditional propositions-as-types AC, which far from being inconsistent is just true (as famously observed by Martin-Lof). There are also the statements considered in Exercise 7.8 of the HoTT Book, which are (apparently) stronger than AC-for-sets but at least some of which are consistent with univalence.

When I wrote the post I wanted to keep it simple and to the point. I was quite sure that the experts will not be able to resist pointing out various alternatives and finer points in the comments. Thanks for living up to the expectation :-)

You are off by one in the last paragraph when you label logic as 0-types and sets as 1-types.

@Jason: Thanks, many people pointed that out. It's been fixed. Another problem is that the universal cover of the circle is contractible and therefore lives at level $-2$ (as Dan Grayson pointed out to me). So maybe I should replace that with the circle.

In the spirit of "living up to your expectations", let me just say that I think you should be careful with statements like "in principle all classical mathematics could be so formalized", because (obviously) practical mathematics really is a lot more than just classical logic + set theory.

I've been reading Terence Tao lately, and greatly enjoy his take on foundational matters. This is from the intro to his review of probability theory:

At a purely formal level, one could call probability theory the study of measure spaces with total measure one, but that would be like calling number theory the study of strings of digits which terminate. At a practical level, the opposite is true: just as number theorists study concepts (e.g. primality) that have the same meaning in every numeral system that models the natural numbers, we shall see that probability theorists study concepts (e.g. independence) that have the same meaning in every measure space that models a family of events or random variables.

And this is from his notes on free probability:

Note that this foundational preference is to some extent a metamathematical one rather than a mathematical one; in many cases it is possible to rewrite the theory in a mathematically equivalent form so that some other mathematical structure becomes designated as the foundational one, much as probability theory can be equivalently formulated as the measure theory of probability measures. However, this does not negate the fact that a different choice of foundations can lead to a different way of thinking about the subject, and thus to ask a different set of questions and to discover a different set of proofs and solutions. Thus it is often of value to understand multiple foundational perspectives at once, to get a truly stereoscopic view of the subject.

I think the real value of the homotopy interpretation of type theory (and I'm sure you would agree :-) is that it adds stereoscopic depth to our understanding of logic and sets. In my mind there is no need to add an "and everything you can do HoTT can do better, in principle".

>even though the HoTT book does not assume excluded middle or choice

Of course, certain theorems do assume this, as part of their hypotheses. You might mention this, as a definitive illustration of doing classical mathematics in HoTT.

>Apparently a mistaken belief has gone viral among certain mathematicians that Univalent foundations is somehow limited to constructive mathematics.

This belief is not only mistaken but downright incoherent. One might as well say that the mistaken belief has gone viral that constructive foundations is limited to constructive mathematics! Of course, there are different varieties of constructive mathematics, but since Bishop's neutral attitude has grown to prominence, most people mean by ‘constructive mathematics’ something that is perfectly compatible with classical mathematics and which becomes classical mathematics upon adding the full axiom of choice (for sets). It is classical mathematics that is limited!

I had quit following that discussion on the list but I'm glad you brought it back to my attention with this post. I really like this post, Andrej.

The greater underlying issue is that you have to be careful how you say things in HoTT. But this is not a new issue: you have to be careful how you say things in all of mathematics. Mathematicians are very familiar with this issue but they are not (yet) familiar with how it plays out in HoTT. Fortunately, mathematicians are well trained at this task. Consciously or not, learning how to correctly handle the vocabulary is one of the very first things one does when approaching a new subject.

I like this post because it emphasizes what you need to be careful with and how to be careful about it when formulating certain things in HoTT. It's not a simple right/wrong issue: it's about how to correctly say what you mean in general. I think this post will actually help the reader to develop some of the reflexes necessary to correctly handle propositions, sets, and other types in HoTT, which are infinitely more valuable skills than just knowing the right formulation of AC and LEM.

By the way, wouldn't it be great if there were some simple examples of higher level types that aren't from topology? I think a compelling example like that would do a lot to promote HoTT.

@Toby: yes, I considered mentioning the sections on cardinals and ordinals which use a lot of excluded middle and choice. Now that someone explicitly mentioned this, I will put in a sentence.

@Noam: did I say that HoTT was better? I said you could formalize "all" classical math in HoTT. You could also do it in Mizar.

I'm not a particularly well-educated in all the variations of constructivism, so I was very surprised to see you write that there are constructivists who expect choice to hold for all types.

1. As Mike noted, the props-as-types/pi-sigma version is simply a theorem of type theory, so I figured you didn't mean that.

2. The set-theoretic version implies classical logic, so I figured you didn't mean that, either.

3. But if you mean a forall/exists version, then it's easy to give models which don't validate it (eg, realizability models for constructive analysis). So it seems like you have to be explicit about what you are assuming and what your intended models are.

But this exhausts the possibilities I know! What kinds of constructivists expect choice to hold in general, and what kind of formulation of choice do they expect?

The statement “Univalent foundations subsume classical mathematics!” begs for a concrete result: Recovering ZF and ZFC/NBG inside HoTT.

It's known that a material set theory is a topos + dssi [Awodey, Butz, Simpson, Streicher '2007], so one could try to show that given a dssi for a particular universe of sets MatSets, the language of material set theory can be naturally interpreted and HoTT is a concervative over CZF/IZF/ZF/ZFC (depending on wether we accept Propositional resizing, LEM for Prop and AC for Set) regarding MatSets. Using the notion of class category, one could probably reconstruct the language of NBG and find a HoTT axiom reassembling NBGs Limitation of Size*, that renders HoTT conservative over NBG. But that's the easy part.

The hard part is to show that advanced all set-theoretic constructions (such as Stone–?ech compactifications, GNS-constructions, weird ultrafilters etc.) can be carried out without using material set theory. The proper formulation would be something like “if a category in its material (MatSet) version admits some universal construction, the structural (“non-evil” in n-cat-lab parlance) version also admits this universal construction.”

(* Limitation of size Axiom of NBG has a highly appealing form: it's a statement allowing “maximal impredicativity” equivalent to the assumption that every category has a basis, i.e. can be represented as a strict category. What's the analogon for HoTT?)

@Neel: where did I state that constructivists accept choice for all types? I said they would ask about choice for all types, because there is a version which holds in type theory, but it is misleading to call that one "choice" in the presence of normal mathematicians. And we are in their presence.

@Alexander: Theorem 10.5.11 of the HoTT book is what you are looking for. It states that there is a 0-type $V$ in HoTT and a relation $\in$ on $V$ such that $(V, {\in})$ is a model of ZFC (assuming choice for $0$-types). One thing I have not mentioned is that there is another "dimension" in HoTT, namely that we postulate a sequence of universes $U_0 \subseteq U_1 \subseteq U_2 \subseteq \cdots$. The $0$-type $V$ that models ZFC can then be constructuted relative to any $U_i$. (It is actually not important whether we get a cummulative sequence of universes or some other variant, but the Univalence axiom is about a universe so we need at least one to express the axiom.)

@Andrej: I'm aware about availability of a ZFC model in HoTT (as well as the classical CZF model in any MLTT, due to Aczel). Depending on what universes are being postulated, there are apparently even bi-interpretability results. But how do we know the given model is a proper embedding? (Such one that the statements provable about the objects of the model and expressible in ZFC-language are exactly the same as the provable ZFC statements?)

It's not clear to me why it should be that way. I'm thinking of T = ZFC + {existence of some inaccessible cardinal ?}, it has a model V_{?+1} of ZFC which is at the same time a model of Morse-Kelley Set Theory. Clearly, the T-provable statements about the objects of the model is at least equal to the set of MK-provable statements and this strictly larger than the set of ZFC-provable statements.

The existence of a conservative model is quite essential for the second part of the question, namely the conjectured fact that any structurally-relevant construction that can be carried out by set-theoretical means, can also be carried out without them.

Regarding Alexander's questions. My understanding is as follows; I hope it is correct. My understanding of the simplicial set model is limited, so I hope that experts will chime in to confirm and/or correct.

In terms of consistency, ZFC + infinitely many inaccessibles proves the consistency of Classical HoTT (HoTT with AC and hence LEM) via the simplicial set construction. On the other hand, for every n, Classical HoTT proves the consistency of ZFC + at least n inaccessibles via the methods of chapter 10 in the book. There is a gap between the two but it is a rather small one and the consistency of Classical HoTT appears to be near the bottom of this gap.

In terms of conservativity, this is much more subtle because of the vast differences between the languages of ZFC and (Classical) HoTT. The problem is that conservativity is about certain classes of statements in a specified language and different choices lead to different conservation results; thus "HoTT is conservative over ZFC + ..." is not completely meaningful without such context. One plausible way of obtaining such a statement is to show that by carrying out the chapter 10 constructions inside the simplicial set model constructed in an ambient model $V$ of ZFC + infinitely many inaccessibles, one can recover the (relevant) $V_\kappa$'s of the ambient model. This seems likely but I cannot be certain since I don't have a sufficient understanding of the simplicial set model to verify. In any case, that would lead to some kind of conservativity results.

It's hard to find all of this, are these issues explicitly addressed somewhere in the HoTT literature?

@Alexander: yes, those are definitely interesting questions, especially the point about structurally-relevant constructions. But I agree with François that we should be careful about formulation of some of the concepts. I don't have anything intelligent to say at this moment.

@François: It ought to be possible to fiddle with the universes. We assume a chain of universes $U_0 \subseteq U_1 \subseteq U_2 \subset \cdots$ out of convenience. We might have $U_\omega$ on top of that. But I suppose then we'd still fall short of the correspondence with $ZFC$ equipped with some inaccessibles. In a way the ZFC $V$ acts like a "top universe", so the right comparison might require a "top universe" on the HoTT side, too.

@Andrej: It's a subtle issue. Mike Shulman and I had a brief discussion about this here. The structure of universes in HoTT has a deep impact on the consistency strength. I had suggested using the minimalist "any two types are in a common universe," and this alternative eventually got mentioned in the book.

To illustrate the subtlety, take the issue of what the indices of the universes actually are, which was brought up in the discussion I linked to. If the indices are purely syntactic, i.e., we have a hierarchy of named universes $U, U', U'',\ldots$ that continues for as many tick marks you can write, then that is essentially the minimalist formulation I proposed with a bunch of extra constant symbols. However, if the indices are elements of the natural number type, then the consistency strength shoots up a little. If formulated appropriately, the consistency of this Classical HoTT implies $\forall n$ Con(ZFC + $n$ inaccessibles) and is therefore strictly stronger than the minimalist Classical HoTT.

Similarly, you get something different if you add $U^\omega$ above all named universes $U,U',U'',\ldots$ than if you have an $U^\infty$ that has a $U:\mathbb{N} \to U^\infty$ such that each $U(n)$ is a universe and every $A:U^\infty$ belongs to some $U(n)$. In fact, you can get some very large cardinal strength by imposing richer structure for the universes...

In any case, the "gap" I mentioned is not an issue for HoTT. There is no reason to expect a natural set theory to be exactly as strong as Classical HoTT in consistency strength. The gap I mentioned is where the consistency of Classical HoTT is. If another theory pops up in this gap, it will be interesting to compare the two, until then, the gap is the end of the story. (More or less, the gap is actually not empty, which is why I said "near the bottom.")

[…] in a comment discussion with Mike Shulman some time ago and they came up again more recently in a comment discussion with Andrej Bauer and Alexander Kuklev. I will use the HoTT book as a reference though this post is not intended as a criticism of the […]

@François, have you considered a version of HoTT with a Mahlo Universe? If I remember correctly, Anton Setzer was able to identify a version of Kripke-Platek Set theory equiconsistent to intensional ML with one Mahlo universe, it would be plausible if classical HoTT with a Mahlo Universe were equiconsistent to ZFC with a Mahlo cardinal.

@Alexander: I looked at that years ago for entirely different reasons and also well before I learned about HoTT. I remember there was a lot to digest at the time and I'm not confident I have the time to immerse myself again. I guess the first question is whether these Mahlo universes are compatible with univalence...

Addendum: I've now mostly convinced myself that the consistency of Classical HoTT (as formulated in the book) is precisely equivalent to the $\Pi_1$-statement $\forall n$Con(ZFC + "there are at least $n$ inaccessibles"). One direction was discussed above and in more detail here. The converse requires a little bit of trickery...

Using compactness, we can get a model of ZFC with a nonstandard natural number $n$ and at least $n$ inaccessibles. Working in this model of ZFC, the simplicial set construction gives a model of type theory with a chain of $n$ univalent universes. Stepping outside this nonstandard model of ZFC, we can forget about the universes indexed by nonstandard numbers and we get a full model of Classical HoTT. Note that the natural numbers $\mathbb{N}$ of this model of Classical HoTT are the same as those of our nonstandard model of ZFC. Thus this argument exploits the very important fact that the universes in HoTT (as formulated in the book) are not indexed by the internal $\mathbb{N}$.

@François, HoTT with a Mahlo universe, given it is compatible with univalence, is interesting for it seems to provide a proper foundations of unlimited category theory in the sense of the equally named article by S. Feferman.

@Alexander: I agree. Universe reflection principles, which is how I would categorize Setzer's Mahlo universe, are potentially very useful and they illustrate the need for "large universe hypotheses."

It's tempting to think that these are only useful for more esoteric purposes. However, I've been to several set theory talks where the speaker said something like: "this is a simple property of subsets of sets of reals, it shouldn't have anything to do with large cardinals." It's only a matter of time until the same kind of thing is said in a HoTT talk.

François asks:

By the way, wouldn’t it be great if there were some simple examples of higher level types that aren’t from topology? I think a compelling example like that would do a lot to promote HoTT.

Thorsten Altenkirch gave a nice talk last week about how the presence of HITs enhances the notion of container/polynomial functor.

Here's a simple example. The walking example of a polynomial functor is that of words, i.e., $W(X) = \sum_{n \in \mathbb{N}} ([n] \to X)$, where $[n]$ denotes the inductive type with $n$ constructors. Usually, an example beyond the reach of polynomial functors is that of finite multisets, i.e., sequences of elements of $X$ up to reordering.

Now let $\mathbb{P}$ denote the HIT defined just like $\mathbb{N}$, but with an identity $n = n$ for each permutation of $[n]$. You get multisets as $M_f(X) = \sum_{p \in \mathbb{P}} ([p] \to X)$.

This is of course a type-theoretic reworking of Joyal's ideas on species, and $\sum$ is really a coend in the last formula.

[…] in a comment discussion with Mike Shulman some time ago and they came up again more recently in a comment discussion with Andrej Bauer and Alexander Kuklev. I will use the HoTT book as a reference though this post is not intended as a criticism of the […]