In a recent lecture at the *Vladimir Voevodsky's Memorial Conference*, Deligne wondered whether "the axioms used are strong enough for the intended purpose." (See his remark from roughly minute 40 in this video: [What do we mean by "equal" ? - by Pierre Deligne](https://www.youtube.com/watch?v=WfDcrN5_1wA).) 


Can anyone comment on his doubt, and class of examples ? Are his worries to be taken seriously ?



Deligne's doubt about Voevodsky's Univalent Foundations
It is a bit difficult to understand what he is asking. The [already-linked nForum discussion](https://nforum.ncatlab.org/discussion/9059/what-is-deligne-asking/) includes some clarification about his example, which at the meeting took us a while to figure out.


More broadly, I think that what he is asking is whether everything we can prove in ZFC about classically-defined homotopy theory (in terms of topological spaces or simplicial sets, say) is also provable in HoTT about *synthetically* defined homotopy theory. As he says, this is not answered by the result that one can construct a model of ZFC inside HoTT, since the classically-defined homotopy theory in that model of ZFC need not coincide with the synthetic homotopy theory in the model of HoTT that we started from.


If HoTT is understood as constructive, without LEM and AC, then the answer to this question is a simple "no": there are things we can prove about classical homotopy theory using LEM and AC that are not provable in constructive synthetic homotopy theory. For instance, as proven by Andreas Blass in *Cohomology detects failures of the axiom of choice*, and reformulated in HoTT [here](https://golem.ph.utexas.edu/category/2013/07/cohomology_detects_failures_of.html), the axiom of choice is equivalent to the statement that every discrete set has vanishing $H^1$ with coefficients in any (not necessarily abelian) group. There are also important open problems in HoTT related to this, e.g. whether it is provable that a set-indexed wedge of circles is always a 1-type (which is true classically, and also in all known models of HoTT, particularly in every Grothendieck $(\infty,1)$-topos, but for which no internal proof in HoTT is known --- as far as I know).


I believe that if we add LEM and AC, the answer is probably still no. There are other "classicality axioms" for synthetic homotopy theory that I would not expect to be implied by LEM+AC, such as Whitehead's principle (a map inducing isomorphisms on all homotopy groups is an equivalence) or [sets cover](https://ncatlab.org/nlab/show/n-types+cover). An example is claimed [here](https://mathoverflow.net/questions/120327/boolean-non-hypercomplete-infty-1-toposes) to show that HoTT+LEM does not imply Whitehead's principle, at least; I am not sure about LEM+AC, but I would be surprised since AC is only a statement about sets.


I think it is a very interesting question whether there is some finite list of "classicality" axioms we can add to HoTT that together ensure everything provable about classical homotopy theory in ZFC is also provable about synthetic homotopy theory in HoTT + those axioms. The combination LEM + AC + Whitehead's principle + sets cover is actually not a bad guess for such a list, since by "sets cover" we might be able to inductively build an internal "simplicial set" surjecting dimensionwise onto any given type and then use Whitehead's principle to show this is a realization equivalence. But that vague idea is a long way from a proof.


So are his worries to be taken seriously? I would say yes, but they should not be considered "worries" but rather *opportunities*! These are interesting research questions that could not even be asked pre-HoTT. If we discover that there is a sufficient list of classicality axioms, then that is a nice theorem that should resolve everyone's "worries". But if we continue discovering new classicality axioms that are not implied by those we already knew, then I think that's an exciting situation too. By expanding the world of mathematical foundations to include higher types, HoTT allows us to formulate and study the relationships between new axioms that didn't even make sense before.


