higher-category-theoryhomotopy-theoryhomotopy-type-theory
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 ?
Perhaps one of the biggest ideas that VV was pursuing is the Initiality Conjecture for Martin-Löf type theory (with universes). A rough idea is that from the rules for a type theory, one can define a category (the syntactic category) that has certain structure depending on which rules are admitted to the type theory. For instance, dependent products correspond to being locally cartesian closed. For any specific type theory, the idea is that the syntactic category it gives rise to is the initial category with that specific structure, in the sense there is a unique functor (preserving appropriate structure) from it to any other such category. What this means is that if one proves a theorem using the type theory, it is automatically true in all categories with that structure. And, vice versa, if it is provable in the language of that kind of structured category, then it is provable in the type theory.
Also, to quote from VV:
"The importance of the initiality conjecture lies in the fact that it provides us with the only known way to prove that type theories such as the Martin-Lof type theories, Calculus of Constructions or Calculus of Inductive Constructions remain consistent after one adds to them axioms such as the axiom of excluded middle or the axiom of choice". (last slide here)
The Initiality Conjecture for MLTT is something that the type theory community expected to be true, based on proofs for much more restricted type theories, but the details of even those were incredibly fearsome. Thomas Streicher wrote a ~300 page book to prove the case of the Calculus of Constructions, a weak subset of the underlying type theory of Coq.
VV's work on mathematising the abstract structure of type theories, so they can be studied and worked with in a proof assistant, was a large part of what he was doing in the last few years. His papers on B- and C-systems [1] were extending work by, for example, Cartmell and others on the type of structure a syntactic category has. Moreover I believe that formal proofs were given for all results in those papers.
Here's a quote by Peter LeFanu Lumsdaine, responding to a criticism by VV of the attitude that "everyone knows the IC is true...":
But I think the second criticism [by VV], on the status of the initiality of the syntactic category, is a bit harder to dismiss. I feel, like you [Mike Shulman] do, that it’s well-established, and we all know how to prove it, it’s just so long and ugly that no-one wants to write it out (and no-one would want to read it). But the more I try to defend it in my head against an imaginary inquisitor, the less comfortable I feel with the situation. “We all know it’s true.” “How? Is it proven?” “Well, no, but it’s a straightforward extension of an existing proof.” “How can you be sure?” “Well, if you understand Streicher’s proof, then you can see it’s easy to extend it.” “Are you sure you’re not missing some details?” “No, there aren’t any tricky details.” “Then why not write it up?” “Well, there are just so many fiddly details…”
So this is one of the things VV was hoping to prove, and formally, so this niggling issue could be put to rest.
[1] Recent published papers include:
see also his arXiv papers.
(Don't be afraid about the word "$\infty$-category" here: they're just a convenient framework to do homotopy theory in).
I'm going to try with a very naive answer, although I'm not sure I understand your question exactly.
The (un)stable motivic ($\infty$-)category has a universal property. To be precise the following statements are true
Theorem: Every functor $E:\mathrm{Sm}_S\to C$ to a(n $\infty$-)category $C$ that
- is $\mathbb{A}^1$-invariant (i.e. for which $E(X\times \mathbb{A}^1)\to E(X)$ is an equivalence)
- satisfies "Mayer-Vietoris for the Nisnevich topology" (i.e. sends elementary Nisnevich squares to pushout squares)
factors uniquely through the unstable motivic ($\infty$-)category.
(see Dugger Universal Homotopy Theories, section 8)
Theorem: Every symmetric monoidal functor $E:\mathrm{Sm}_S\to C$ to a pointed presentable symmetric monoidal ($\infty$-)category that
- is $\mathbb{A}^1$-invariant
- satisfies "Mayer-Vietoris for the Nisnevich topology"
- sends the "Tate motive" (i.e. the summand of $E(\mathbb{P}^1)$ obtained by splitting off the summand corresponding to $E(\mathrm{Spec}S)\to E(\mathbb{P}^1)$) to an invertible object
factors uniquely through the stable motivic ($\infty$-)category.
(see Robalo K-Theory and the bridge to noncommutative motives, corollary 2.39)
These two theorems are saying that any two functors that "behave like a homology theory on smooth $S$-schemes" will factor uniquely through the (un)stable motivic ($\infty$-)category. Examples are $l$-adic étale cohomology, algebraic K-theory (if $S$ is regular Noetherian), motivic cohomology (as given by Bloch's higher Chow groups)... Conversely, the canonical functor from $\mathrm{Sm}_S$ to the (un)stable motivic ($\infty$-)category has these properties. So the (un)stable motivic homotopy theory is in this precise sense the home of the universal homology theory. In particular all the properties we can prove for $\mathcal{H}(S)$ or $SH(S)$ reflect on every homology theory satisfying the above properties (purity being the obvious example).
Let me say a couple of words about the two aspects that "worry you"
$\mathbb{A}^1$-invariance needs to be imposed. That's not surprising: we do need to do that also for topological spaces, when we quotient the maps by homotopy equivalence (or, more precisely, we need to replace the set of maps by a space of maps, where paths are given by homotopies: this more complicated procedure is also responsible for the usage of simplicial presheaves rather than just ordinary presheaves)
Having more kinds of spheres is actually quite common in homotopy theory. A good test case for this is $C_2$-equivariant homotopy theory. See for example this answer of mine for a more detailed exploration of the analogy.
Surprisingly, possibly the most problematic of the three defining properties of $SH(S)$ is the $\mathbb{A}^1$-invariance. In fact there are several "homology theories" we'd like to study that do not satisfy it (e.g. crystalline cohomology). I know some people are trying to find a replacement for $SH(S)$ where these theories might live. As far as I know there are some definitions of such replacements but I don't think they have been shown to have properties comparable to the very interesting structure you can find on $SH(S)$, so I don't know whether this will bear fruit or not in the future.
Best Answer
It is a bit difficult to understand what he is asking. The already-linked nForum discussion 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, 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. An example is claimed here 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.