[Math] Vladimir Voevodsky’s works

Question

Vladimir Voevodsky has made several contributions in abstract algebraic geometry, focused on the homotopy theory of schemes, algebraic K-theory, and interrelations between algebraic geometry, and algebraic topology.

Voevodsky was awarded the Fields Medal in 2002. Sadly, he died September 30, 2017.

Can one draw a general picture of his works?

Any expository reference will be appreciated.

Answer 1

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:

• C-systems defined by universe categories: presheaves
• The $(\Pi,\lambda)$-structures on the C-systems defined by universe categories
• Products of families of types and $(\Pi,\lambda)$-structures on C-systems
• A C-system defined by a universe category

see also his arXiv papers.