Deligne's doubt about Voevodsky's Univalent Foundations

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.)

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

• I believe I watched that video, but can't recall the comment (I'll have to check out the time stamp you mention)—but HoTT+AC proves at least the consistency of ZFC (and even, for every $n$, the consistency of ZFC+$\exists\, n$ inaccessible cardinals). When I check the video I will measure up the examples against this. – David Roberts Mar 1 '19 at 15:30
• There was a short discussion of this on the n-forum: nforum.ncatlab.org/discussion/9059/what-is-deligne-asking – Michael Bächtold Mar 1 '19 at 17:00
• You may also look at Mirna Dzamonja's paper "A new foundational crisis in mathematics, is it really happening". – Mohammad Golshani Mar 2 '19 at 10:58
• @MohammadGolshani I would not recommend that paper. – Mike Shulman Mar 8 '19 at 5:28
• @ThomasKlimpel That's precisely one of the statements that I believe to be a caricature. I have never heard anyone in the HoTT community make any such claim, nor do I think it sensible to imagine that HoTT has anything to do with computers "doing our mathematics for us". To be sure there are people who believe that that is the future of mathematics, but they have nothing to do with HoTT as far as I know. – Mike Shulman Mar 11 '19 at 11:40

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, 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).