Publications - Vladimir Voevodsky

We include here Voevodsky's published and unpublished papers, letters, and videos and slides of talks, in roughly chronological order. More items are listed here than on his home page, which has been essentially static since his death, but don't neglect to look there also, for we haven't included everything that is there. Items include links to preprint versions, reviews, and his working files, including TeX files.

The same list as this one, but without abstracts, is visible here.

We've indicated the current status of those papers submitted for publication and undergoing review or revision.

The entry numbers are assigned sequentially when this page is remade from the bibtex source file, and should not be expected to be unchanging. However, the (invisible) symbolic labels for each entry will be preserved and can be used in a link, such as this one: MR2811603, which links to On motivic cohomology with ℤ/l-coefficients. Click on a number to get the link.


[1] V. A. Voevodskiĭ and G. B. Shabat. Equilateral triangulations of Riemann surfaces, and curves over algebraic number fields. Dokl. Akad. Nauk SSSR, 304(2):265--268, 1989. [ bib | MR | pdf ]
[2] V. A. Voevodsky. Galois group over ℚ and Teichmüller modular groups. In Proc. Conf. Constr. Methods and Alg. Number Theory, Minsk, 1989. [ bib ]
[3] V. A. Voevodsky. Triangulations of Oriented Manifolds and Ramified Coverings of Sphere (in Russian). In Proc. Conf. of Young Scientists. Moscow Univ. Press, 1990. [ bib ]
[4] V. A. Voevodsky and G. B. Shabat. Piece-wise Euclidean Approximation of Jacobians of Algebraic Curves. 1990. CSTARCI Math. Preprints. [ bib | pdf ]
[5] V. A. Voevodsky. Flags and Grothendieck Cartographical Group in Higher Dimensions. 1990. CSTARCI Math. Preprints. Translation by George Shabat. [ bib | Russian pdf | pdf ]
[6] V. A. Voevodsky and M. M. Kapranov. Multidimensional categories (in Russian). In Proc. Conf. of Young Scientists. Moscow Univ. Press, 1990. [ bib ]

This paper existed only in hand-written form, and we don't have a copy.

[7] V. A. Voevodskiĭ and M. M. Kapranov. ∞-группоиды как модель для гомотопической категории. (∞-groupoids as a model for a homotopy category). Uspekhi Mat. Nauk, 45(5(275)):183--184, 1990. [ bib | DOI | MR | Russian pdf | pdf | ZB | http ]

A later paper is an expanded version of this one.

Warning: the main theorem of this paper was shown by Carlos Simpson to be false. See https://arxiv.org/abs/math/9810059. See also sections 2.3-2.7 of Simpson's book, "Homotopy theory of higher categories", New Mathematical Monographs, volume 19, Cambridge University Press, Cambridge, 2012. See also the paper by Simon Henry -- he carries through the Voevodsky-Kapranov approach.

[8] G. B. Shabat and V. A. Voevodsky. Drawing curves over number fields. In The Grothendieck Festschrift, Vol. III, volume 88 of Progr. Math., pages 199--227. Birkhäuser Boston, Boston, MA, 1990. [ bib | DOI | MR | pdf ]
[9] V. A. Voevodskiĭ. Étale topologies of schemes over fields of finite type over ℚ. Izv. Akad. Nauk SSSR Ser. Mat., 54(6):1155--1167, 1990. [ bib | DOI | MR | Russian pdf | pdf | http ]

The author proves a conjecture of Grothendieck concerning the possibility of recovering a normal scheme over a field of finite type over ℚ from its étale site.

[10] V. A. Voevodskiĭ and M. M. Kapranov. The free n-category generated by a cube, oriented matroids and higher Bruhat orders. Funktsional. Anal. i Prilozhen., 25(1):62--65, 1991. [ bib | DOI | MR | Russian pdf | pdf | http ]

In investigating multidimensional generalizations of the Yang-Baxter equation, in three papers Manin and Shekhtman introduced partially ordered sets B(n,k) called higher Bruhat orders. The set B(n,i) is the symmetric group Sn with its weak Bruhat order, and B(n,k+1) is obtained by a factorization from the set of maximal chains in B(n,k). In their papers the connection was pointed out for B(n,k) with arrangements of n hyperplanes in ℝk in general position and also with the structure of the convex hull of a general orbit of Sn in ℝn. In the present note we give an interpretation of B(n,k) as the sets of some k-dimensional strips in an n-dimensional cube. This permits us to clarify the above-mentioned connections, in particular to prove a hypothesis from their papers and disprove another hypothesis of theirs.

[11] M. M. Kapranov and V. A. Voevodsky. Combinatorial-geometric aspects of polycategory theory: pasting schemes and higher Bruhat orders (list of results). Cahiers Topologie Géom. Différentielle Catég., 32(1):11--27, 1991. International Category Theory Meeting (Bangor, 1989 and Cambridge, 1990). [ bib | MR | pdf | http ]

This talk is devoted to detailed study of free n-categories and their relations with more "classical" geometric objects. Among these objects we list convex polytopes, their triangulations, configurations of hyperplanes, oriented matroids, and so-called "higher Bruhat orders", introduced by Y. I. Manin and V. V. Schechtman. The base for our study is the notion of a pasting diagram for n-categories introduced by M. Johnson. Though we feel that much of Johnson's theory can be substantially simplified, even in its present state it yields a lot of combinatorial objects, some of which are known, and the others new and unexpected.

[12] M. M. Kapranov and V. A. Voevodsky. ∞-groupoids and homotopy types. Cahiers Topologie Géom. Différentielle Catég., 32(1):29--46, 1991. International Category Theory Meeting (Bangor, 1989 and Cambridge, 1990). [ bib | MR | pdf | http ]

An earlier paper is an announcement preceding this one.

Warning: the main theorem of this paper was shown by Carlos Simpson to be false. See https://arxiv.org/abs/math/9810059. The error probably lies in the proof of Lemma 3.4. See also sections 2.3-2.7 of Simpson's book, "Homotopy theory of higher categories", New Mathematical Monographs, volume 19, Cambridge University Press, Cambridge, 2012. See also the paper by Simon Henry -- he carries through the Voevodsky-Kapranov approach.

[13] V. A. Voevodskiĭ. Galois groups of function fields over fields of finite type over ℚ. Uspekhi Mat. Nauk, 46(5(281)):163--164, 1991. [ bib | DOI | MR | Russian pdf | pdf | ZB | http ]
[14] V. A. Voevodskiĭ. Galois representations connected with hyperbolic curves. Izv. Akad. Nauk SSSR Ser. Mat., 55(6):1331--1342, 1991. [ bib | DOI | MR | Russian pdf | pdf | ZB | http ]

The author considers Galois group actions on the fundamental groups of curves of hyperbolic type, and proves certain cases of Grothendieck's conjecture about the possibility of recovering a curve from its Galois representation.

[15] Vladimir Voevodsky. A letter to Beilinson, December 6, 1992. [ bib | preprint ]
[16] Vladimir Voevodsky. Homology of schemes and covariant motives. ProQuest LLC, Ann Arbor, April, 1992. Ph.D. Thesis, Harvard University. [ bib | MR | pdf | http ]

The pdf file is an optical scan with OCR, and the cross-references are broken and print as question marks. We would like to find a digital version.

[17] M. Kapranov and V. Voevodsky. Braided monoidal 2-categories and Manin-Schechtman higher braid groups. J. Pure Appl. Algebra, 92(3):241--267, 1994. [ bib | DOI | MR | pdf ]

We study a certain coherence problem for braided monoidal 2-categories. For ordinary braided monoidal categories such a problem is well known to lead to braid groups: If we denote by T(n) the pure braid group on n strands then this group acts naturally on each product A1 ⊗ ··· ⊗ An. It turns out that in the 2-categorical case we have to consider the so-called higher braid group T(2,n) introduced by Manin and Schechtman. The main result is that T(2,n) naturally acts by 2-automorphisms on the canonical 1-morphism A1 ⊗ ··· ⊗ An → An ⊗ ··· ⊗ A1 for any objects A1, ..., An.

[18] M. M. Kapranov and V. A. Voevodsky. 2-categories and Zamolodchikov tetrahedra equations. In Algebraic groups and their generalizations: quantum and infinite-dimensional methods (University Park, PA, 1991), volume 56 of Proc. Sympos. Pure Math., pages 177--259. Amer. Math. Soc., Providence, RI, 1994. [ bib | MR | pdf ]
[19] V. Voevodsky. A nilpotence theorem for cycles algebraically equivalent to zero. Internat. Math. Res. Notices, (4):187--198, 1995. [ bib | DOI | preprint | MR | pdf ]

In this paper we prove that a correspondence from a smooth projective variety over a field to itself, which is algebraically equivalent to zero, is nilpotent in the ring of correspondences modulo rational equivalence (with rational coefficients).


Claire Voisin has proved a slightly stronger version of the nilpotence theorem, independently, in the paper Remarks on zero-cycles of self-products of varieties, in the book "Moduli of vector bundles (Sanda, 1994; Kyoto, 1994)", 265-285, Lecture Notes in Pure and Appl. Math., 179, Dekker, New York, 1996.

[20] Vladimir Voevodsky. Four functors formalism. March, 1999. Unpublished, 20 pages. [ bib | .pdf ]

One of the most important ideas of the four functor formalism was the proof that a projective morphism is lower transversal (satisfies a generalized analog of the proper base change theorem). Unfortunately no complete proof remained, but all of the main ideas are contained in these notes:

[21] Andrei Suslin and Vladimir Voevodsky. Singular homology of abstract algebraic varieties. Invent. Math., 123(1):61--94, 1996. [ bib | DOI | preprint | MR | pdf ]

The main objective of the present paper is to construct a reasonable singular homology theory on the category of schemes of finite type over an arbitrary field k.

[22] V. Voevodsky. Homology of schemes. Selecta Math. (N.S.), 2(1):111--153, 1996. [ bib | DOI | preprint | MR | pdf ]

In this paper we suggest an approach to the construction of the category of mixed motives. The word "motive" was introduced by A. Grothendieck almost thirty years ago to denote objects of the hypothetical semi-simple Q-linear abelian category where the "universal" cohomology theory on the category of smooth projective algebraic varieties takes values. Some fifteen years later the Grothendieck's idea was developed further by P. Deligne, A. Beilinson, S. Lichtenbaum and others to accommodate all algebraic varieties. These new "motives" were called "mixed motives" after the mixed Hodge structures and old Grothendieck's motives were renamed into "pure motives". For all these years the theory of motives was one of the most important unification concepts in algebraic geometry. In its modern form it gives a very coherent picture of how cohomology theories on the category of algebraic varieties should behave. In particular, it provides a natural "explanation" for many apparently unrelated conjectures such as the Bloch-Kato conjecture in the étale cohomology, the Quilten-Lichtenbaum conjecture and the Beilinson-Soulé vanishing conjecture in the algebraic K-theory, the Bloch conjecture on zero cycles and the Grothendieck standard conjectures in the theory of algebraic cycles etc.

Unfortunately, until very recently, the theory of motives and especially the theory of mixed motives remained almost totally hypothetical. While quite a few results which confirmed the feeling that such a theory should exist were obtained no candidates for the category of mixed motives over an arbitrary field were suggested and none of the "standard conjectures" were proved.

This paper is the first one in a series of related papers where we try to develop techniques necessary to construct the theory of (mixed) motives. The fundamental difference of the approach considered here with the one usually used is that we construct a triangulated category of mixed motives instead of the abelian category required by the standard conjectures.

[23] Vladimir Voevodsky. 𝔸1-homotopy theory. In Proceedings of the International Congress of Mathematicians, Vol. I (Berlin, 1998), number Extra Vol. I, pages 579--604, 1998. [ bib | MR | pdf | .html ]
[24] V. Voevodsky. Voevodsky's Seattle lectures: K-theory and motivic cohomology. In Algebraic K-theory (Seattle, WA, 1997), volume 67 of Proc. Sympos. Pure Math., pages 283--303. Amer. Math. Soc., Providence, RI, 1999. Notes by C. Weibel. [ bib | DOI | preprint | MR | pdf ]

These notes are based on a series of talks given by V. Voevodsky at the AMS Joint Summer Research Conference on algebraic K-theory, held in Seattle during July 1997. The purpose of these talks was to outline the proof of "Milnor's conjecture."

[25] Vladimir Voevodsky. Categories and functors in mathematics. 1999. Unpublished. [ bib | files | pdf ]

Follow the "files" link to see a second version of the paper.

[26] Fabien Morel and Vladimir Voevodsky. 𝔸1-homotopy theory of schemes. Inst. Hautes Études Sci. Publ. Math., (90):45--143 (2001), 1999. [ bib | preprint | MR | pdf | http ]

In this paper we begin to develop a machinery which we call 𝔸1-homotopy theory of schemes. All our constructions are based on the intuitive feeling that if the category of algebraic varieties is in any way similar to the category of topological spaces then there should exist a homotopy theory of algebraic varieties where affine line plays the role of the unit interval.

[27] Vladimir Voevodsky. Sheaves and sheaves with transfers in the cdh-topology, November 9, 1999. 23 pages. An unfinished unreleased note. [ bib | files | pdf ]

These unfinished notes are a byproduct of the paper on cohomological operations. It can be developed into a paper about general properties of sheaves and sheaves with transfers in the cdh-topology on the categories of schemes over a base.

[28] Andrei Suslin and Vladimir Voevodsky. Bloch-Kato conjecture and motivic cohomology with finite coefficients. In The arithmetic and geometry of algebraic cycles (Banff, AB, 1998), volume 548 of NATO Sci. Ser. C Math. Phys. Sci., pages 117--189. Kluwer Acad. Publ., Dordrecht, 2000. [ bib | preprint | MR | pdf | http ]

An earlier version of the preprint is here: 0083.

In this paper we prove the equivalence of two well known conjectures - the Bloch-Kato conjecture which asserts that the cotorsion in Milnor's K-groups of a field is isomorphic to its etale cohomology and the Beilinson-Lichtenbaum conjecture which provides a complete description of the motivic cohomology with finite coefficients in terms of the etale cohomology. Since the Bloch-Kato conjecture is known in dimension 2 (and in dimension 3 for ℤ/2-coefficients) we obtain in particular a proof of the Beilinson-Lichtenbaum conjecture in weight 2 and in weight 3 for ℤ/2-coefficients.

[29] Vladimir Voevodsky, Andrei Suslin, and Eric M. Friedlander. Cycles, transfers, and motivic homology theories, volume 143 of Annals of Mathematics Studies. Princeton University Press, Princeton, NJ, 2000. [ bib | preprint | MR ]

This is a book, each of whose chapters is listed separately.

[30] Eric M. Friedlander, A. Suslin, and V. Voevodsky. Introduction. In Cycles, transfers, and motivic homology theories, volume 143 of Ann. of Math. Stud., pages 3--9. Princeton Univ. Press, Princeton, NJ, 2000. [ bib | preprint | MR | pdf | http ]

Our original goal which finally led to this volume was the construction of "motivic cohomology theory" whose existence was conjectured by A. Beilinson and S. Lichtenbaum. Even though this would seem to be achieved at the end of the third paper, our motivation evolved into a quest for a deeper understanding of various properties of algebraic cycles. Thus, several of the papers presented here do not deal directly with motivic cohomology but rather with basic questions about algebraic cycles.

[31] Andrei Suslin and Vladimir Voevodsky. Relative cycles and Chow sheaves. In Cycles, transfers, and motivic homology theories, volume 143 of Ann. of Math. Stud., pages 10--86. Princeton Univ. Press, Princeton, NJ, 2000. [ bib | earlier preprint | preprint | MR | pdf | http ]

For a scheme X of finite type over a Noetherian scheme S we define a group of relative equidimensional cycles. We show that it is contravariantly functorial with respect to base change and thus provides a presheaf on the category of Noetherian schemes over S. Moreover this presheaf turns out to be a sheaf in a Grothendieck topology called the cdh-topology. The main goal of the paper is to study these Chow sheaves. In the particular case of X being a projective variety over a field of characteristic zero the Chow sheaf of effective cycles of dimension d is representable by the corresponding Chow variety. Even in this case though it turns out to be more convenient to work with sheaves than with varieties. In particular we construct certain short exact sequences of Chow sheaves which in the case of varieties over a field lead to localization long exact sequences in algebraic cycle homology and which do not have any obvious analog for Chow varieties.

[32] Vladimir Voevodsky. Cohomological theory of presheaves with transfers. In Cycles, transfers, and motivic homology theories, volume 143 of Ann. of Math. Stud., pages 87--137. Princeton Univ. Press, Princeton, NJ, 2000. [ bib | preprint | MR | pdf | http ]

In this paper we study a class of functors called pretheories on the category of smooth schemes over a perfect field. Morally, a pretheory is a contravariant functor equipped with transfers with respect to relative divisors with compact support on smooth relative curves. Among the examples of such functors are K-cohomology, bivariant cycle homology of Friedlander and Gabber ("Cycle spaces and intersection theory", in the book "Topological Methods in Modern Mathematics") and in some sense algebraic singular homology (see "Singular homology of abstract algebraic varieties", by Suslin and Voevodsky). Our main result states that Zariski cohomology with coefficients in a homotopy invariant pretheory is again a homotopy invariant pretheory. Together with some other properties of pretheories this result allows us to prove the Mayer-Vietoris property for algebraic singular homology and in the case when there is resolution of singularities to prove the localization property for algebraic cycle homology. One of the most important technical tools which allows us to deal effectively with pretheories is the Nisnevich topology on algebraic varieties.


An earlier preprint is available here, under a different title: Homology of schemes, II. In The Origins and Motivations of Univalent Foundations and in the slides for a talk at the IAS, Voevodsky says that the proof of a key lemma (Lemma 4.22) in that earlier preprint and in this one (Lemma 4.23), is wrong, and that a corrected argument was published in Lecture notes on motivic cohomology as Lemma 22.10.

[33] Eric M. Friedlander and Vladimir Voevodsky. Bivariant cycle cohomology. In Cycles, transfers, and motivic homology theories, volume 143 of Ann. of Math. Stud., pages 138--187. Princeton Univ. Press, Princeton, NJ, 2000. [ bib | earlier preprint | preprint | MR | pdf | http ]

In this paper we construct a bivariant (co-)homology theory on the category of algebraic varieties over a field which admits resolution of singularities. We show that this theory has the standard good properties, such as localization long exact sequences (with respect to the covariant argument) and Mayer-Vietories long exact sequences (with respect to the contravariant argument). We also prove the duality theorem which asserts that for smooth varieties the corresponding covariant and contravariant theories are isomorphic. We further use it to define four "motivic (co-)homology" theories (motivic homology, Borel-Moore motivic homology, motivic cohomlogy and motivic cohomology with compact supports) which are related by duality isomorphisms in the smooth case.

[34] Vladimir Voevodsky. Triangulated categories of motives over a field. In Cycles, transfers, and motivic homology theories, volume 143 of Ann. of Math. Stud., pages 188--238. Princeton Univ. Press, Princeton, NJ, 2000. [ bib | even earlier preprint | earlier preprint | preprint | MR | pdf | http ]

In this paper we define and study the triangulated category of mixed motives over a field. At least in the case when there is resolution of singularities, we are able to prove that this category is has a natural duality and that the Hom-groups between Tate objects are canonically isomorphic to the corresponding higher Chow groups. A detailed of summary of results of the paper is given in the first section.

[35] Vladimir Voevodsky. On 2-torsion in motivic cohomology. July, 2001. [ bib | preprint ]

In this paper we prove the 2-local part of the Beilinson-Lichtenbaum conjectures on tosion in motivic cohomology. In particular we prove the Milnor conjecture relating Milnor's K-theory and the Galois cohomology with ℤ/2-coefficients. This paper is a new version of the previously distributed preprint "The Milnor Conjecture".

This unpublished paper contains an earlier version of the proof published in "Motivic cohomology with ℤ/2-coefficients".

[36] Pierre Deligne. Voevodsky's lectures on cross functors. Fall, 2001. Unpublished. [ bib | .pdf ]
[37] Vladimir Voevodsky. Framed correspondences. November, 2001. Unpublished. [ bib | files | .pdf ]

The simplest way to motivate the necessity of the motivic stable homotopy category is to refer to the fact that algebraic K-theory does not extend to the the triangulated category of motives. In particular the triangulated category of motives does not provide a sufficient framework to study such a fundamental object as the motivic spectral sequence. The other motivation comes from the cohomological operations but for historic reasons it seems to be less useful.

I hope that the constructions described in these notes will lead to a new model of the stable homotopy theory which will be more friendly for computations questions. Of course one expects that it will be nontrivial to show that the new and the old models agree.


Note: this unpublished work of Voevodsky's was used fruitfully in 1409.4372, 1504.00884, 1601.06642, and 1604.02732 to develop a theory of "framed motives". The first paper of the series states that Vladimir shared this work with them in 2010, and Panin says that shortly after Vladimir heard Panin's talk at the IAS on the topic in March, 2015, he made the notes available on his home page.

[38] Vladimir Voevodsky. Motivic cohomology groups are isomorphic to higher Chow groups in any characteristic. Int. Math. Res. Not., (7):351--355, 2002. [ bib | DOI | preprint | MR | pdf ]

In this paper we prove that two definitions of motivic cohomology for smooth varieties over any field agree. The first definition is the one used in the proof of the Milnor conjecture. The second one was shown by Friedlander and Suslin to agree with Bloch's higher Chow groups. A proof of the main theorem of this paper was previously known for varieties over fields with resolution of singularities.

[39] Vladimir Voevodsky. A possible new approach to the motivic spectral sequence for algebraic K-theory. In Recent progress in homotopy theory (Baltimore, MD, 2000), volume 293 of Contemp. Math., pages 371--379. Amer. Math. Soc., Providence, RI, 2002. [ bib | DOI | preprint | MR | pdf ]

We describe a simple construction of the spectral sequence relating algebraic K-theory and motivic cohomology modulo two general conjectures on the structure of the motivic homotopy category. The first conjecture is the motivic analog of the fact that the zero stage of the Postnikoff tower for the (topological) sphere spectrum is the Eilenberg-Maclane spectrum H. The second is the motivic analog of the fact that the functor Ω1Σ1 takes n-connected spaces to n-connected spaces.

[40] Vladimir Voevodsky. Open problems in the motivic stable homotopy theory. I. In Motives, polylogarithms and Hodge theory, Part I (Irvine, CA, 1998), volume 3 of Int. Press Lect. Ser., pages 3--34. Int. Press, Somerville, MA, 2002. [ bib | preprint | MR | pdf | http ]

In this paper we discuss a number of conjectures concentrated around the notion of the slice filtration and the related notion of the rigid homotopy groups. Many of the ideas discussed below are in greater or lesser degree the result of conversations I had with Fabien Morel, Mike Hopkins and, more recently, Charles Rezk.

[41] Vladimir Voevodsky. Reduced power operations in motivic cohomology. Publ. Math. Inst. Hautes Études Sci., (98):1--57, 2003. [ bib | DOI | earlier preprint | preprint | MR | pdf ]

In this paper we construct an analog of Steenrod operations in motivic cohomology and prove their basic properties including the Cartan formula, the Adem relations and the realtions to characteristic classes.

[42] Vladimir Voevodsky. Motivic cohomology with ℤ/2-coefficients. Publ. Math. Inst. Hautes Études Sci., (98):59--104, 2003. [ bib | DOI | MR | pdf ]

There were several papers that preceded this paper that explored other proofs of the Milnor Conjecture based on the same general direction of approach. Ultimately it was the present paper that was published in a journal since the proof that it contained was most direct and required the least amount of preliminary work. The earlier versions of the proof are available here:

[43] V. Voevodsky. On the zero slice of the sphere spectrum. Tr. Mat. Inst. Steklova, 246:106--115, 2004. [ bib | earlier preprint | preprint | MR | pdf | ZB | http ]

In this paper we prove over fields of characteristic zero that the zero slice of the motivic sphere spectrum is the motivic Eilenberg-Maclane spectrum. As a corollary one concludes that the slices of any spectrum are modules over the motivic Eilenberg-MacLane spectrum. To prove our result we analyze the unstable homotopy type of the symmetric powers of the T-sphere.

[44] Категорный поход к теории вероятностей -- A categorical approach to the theory of probability (in Russian), September 2, 2004. A talk in the A. Bondal Seminar. [ bib | http ]
[45] Historic inference from non-recombinant genetic data, March 6, 2006. 4 pages. An unfinished unreleased manuscript. [ bib | files | pdf ]

This text contains a preliminary description of the algorithms for generating sample non-recombinant genealogies from demographic parameters (birth and death rates), for reconstructing these genealogies from their genomic images and for reconstructing the demographic parameters from the genealogies.

[46] What can the genetic data tell us about the history?, March 6, 2006. 3 pages. An unfinished unreleased manuscript. [ bib | files | pdf ]

There are two kinds of histories. Histories of the first kind concentrate on a small number of key individuals and interpret the past events through their relation to these individuals. Histories of the second kind are concerned more with the dynamics of large groups of people - migrations, expansions or contractions of whole populations, changes in customs, culture and technology etc. The modern advances in our ability to extract information from the genomes can help to construct booth kinds of histories. Here we are concerned mostly with the histories of the second kind.

[47] Vladimir Voevodsky. On an approach to conveniently formalize mathematics, March 5, 2006. An unfinished paper. [ bib | files | pdf ]

In these preliminary notes, Voevodsky presents a proposal for a formal language for mathematics. Within a year, however, he chose dependent type theory as the ideal formal language, abandoning this project.

[48] Vladimir Voevodsky. Notes on homotopy λ-calculus. March 25, 2006. Unpublished, 70 pages. [ bib | files | pdf ]

In this paper we suggest a new approach to the foundations of mathematics. In fact the adjective "new" in the previous sentence may be superfluous since one can argue that pure mathematics as it is practiced today has no foundations. We have come a long way from where we used to be at the beginning of the century when the thesis that mathematics is that which can be formalized in the framework of the Zermelo-Fraenkel theory became generally accepted. Contemporary constructions and proofs can not be translated in any sensible way into the Zermelo-Fraenkel theory. One can (may be!) translate the categorical definition of group cohomology into the ZF-theory using the Grothendieck’s idea of universes but it is hardly fair to call an approach which requires one to believe in strongly unreachable cardinals in order to interpret a simple algebraic construction sensible.


Voevodsky posted an earlier version on github.

[49] Carlo Mazza, Vladimir Voevodsky, and Charles Weibel. Lecture notes on motivic cohomology, volume 2 of Clay Mathematics Monographs. American Mathematical Society, Providence, RI; Clay Mathematics Institute, Cambridge, MA, 2006. [ bib | preprint | MR | pdf | .pdf ]

This book was written by Carlo Mazza and Charles Weibel on the basis of the lectures on motivic cohomology which I gave at the Institute for Advanced Study in Princeton in 1999/2000.

[50] Vladimir Voevodsky. A very short note on homotopy λ-calculus. September, 2006. Unpublished, 7 pages. [ bib | files | .pdf ]

This is the first preprint where Voevodsky puts down his ideas about univalence.

[51] D. Orlov, A. Vishik, and V. Voevodsky. An exact sequence for KM*/2 with applications to quadratic forms. Ann. of Math. (2), 165(1):1--13, 2007. [ bib | DOI | earlier preprint | preprint | MR | pdf ]

We construct a four-term exact sequence which provides information on the kernel and cokernel of the multiplication by a pure symbol in Milnor's K-theory mod 2 of fields of characteristic zero. As an application we establish, for fields of characteristics zero, the validity of three conjectures in the theory of quadratic forms - the Milnor conjecture on the structure of the Witt ring, the Khan-Rost-Sujatha conjecture and the J-filtration conjecture. The first version of this paper was written in the spring of 1996.

[52] B. I. Dundas, M. Levine, P. A. Østvær, O. Röndigs, and V. Voevodsky. Motivic homotopy theory. Universitext. Springer-Verlag, Berlin, 2007. Lectures from the Summer School held in Nordfjordeid, August 2002. [ bib | DOI | MR | pdf ]

Motivic homotopy theory is a new and in vogue blend of algebra and topology. Its primary object is to study algebraic varieties from a homotopy theoretic viewpoint. Many of the basic ideas and techniques in this subject originate in algebraic topology.

This text is a report from Voevodsky's summer school lectures on motivic homotopy in Nordfjordeid. Its first part consists of a leisurely introduction to motivic stable homotopy theory, cohomology theories for algebraic varieties, and some examples of current research problems. As background material, we recommend the lectures of Dundas [Dun] and Levine [Lev] in this volume. An introductory reference to motivic homotopy theory is Voevodsky's ICM address [Voe98]. The appendix includes more in depth background material required in the main body of the text. Our discussion of model structures for motivic spectra follows Jardine's paper.

[53] Vladimir Voevodsky, Oliver Röndigs, and Paul Arne Østvær. Voevodsky's Nordfjordeid lectures: motivic homotopy theory. In Motivic homotopy theory, Universitext, pages 147--221. Springer, Berlin, 2007. [ bib | DOI | MR ]
[54] Категорная вероятность -- Categorical probability (in Russian), November 20, 2008. A talk in the Steklov Mathematical Institute Seminar. [ bib | video ]

In early 60's Bill Lawvere defined a category whose objects are measurable spaces and morphisms are Markov kernels. I will try to show how this category allows one to think about many of the notions of probability theory in categorical terms and to connect probabilistic objects to objects of other types through various functors.

[55] Категорная вероятность II -- Categorical probability II (in Russian), November 25, 2008. A talk in the Seminar of the Department of Algebra. [ bib | http ]
[56] Синглетоны -- Singletons (in Russian), November 27, 2008. A talk in the Seminar of the Department of Mathematical Physics, Steklov Mathematical Institute of RAS. [ bib | http ]

Я опишу модель, в рамках которой можно исследовать вопрос о возможности восстановления истории популяции по её генетической структуре.

[57] Notes on categorical probability, July 13, 2009. 75 pages. An unfinished unreleased manuscript. [ bib | files | pdf ]

This paper of Voevodsky's seems to introduce concepts and facts used in Singletons, such as path system, process, Markov pre-process.

[58] Singletons, May 11, 2009. 94 pages. An unfinished unreleased manuscript. [ bib | files | pdf ]

The goal of this paper is to solve the following problem. Consider a population of identical ageless individuals (singletons) where each individual can go through one of the two possible transformations - it can die or it can divide into two. Suppose that the past history of the population was determined by the conditions that the birth (division) rate was constant and equal to 1 and the death rate was an unknown function of time d(t). Suppose further that we know the ancestral tree of the present day population, i.e., for each pair of singletons we know the time distance from the present to their "last common ancestor". Given this data what is the maximal likelihood reconstruction of the death rate function?


In an interview with Roman Mikhailov in 2012, Voevodsky said, of this work: "В результате я выбрал, как сейчас понимаю неправильно, проблему восстановления истории популяций по их современной генетической композиции. Я провозился с этой задачей в общей сложности около двух лет и в конце концов, уже в 2009 году, понял, что то, что я придумывал, бесполезно. В моей жизни, пока, это была, пожалуй, самая большая научная неудача. Очень много работы было вложено в проект, который полностью провалился. Какая-то польза, конечно, все-таки, была - я выучил много из теории вероятности, которую знал плохо, а также узнал много нового про демографию и демографическую историю."

Google-translate renders that as "As a result, I chose, as I now understand incorrectly, the problem of restoring the history of populations according to their modern genetic composition. I took on this task for a total of about two years, and in the end, already in 2009, I realized that what I was inventing was useless. In my life, so far, it was, perhaps, the greatest scientific failure. A lot of work was invested in the project, which completely failed. Of course, there was some benefit, of course - I learned a lot from probability theory, which I knew badly, and also learned a lot about demography and demographic history."

[59] Системы путей -- Systems of paths (in Russian), August 25, 2009. A talk in the Seminar of the Department of Algebra. [ bib | http ]

Системой путей на временно́м интервале T со значением в категории C называется контравариантный функтор на категории под-интервалов в T, упорядоченных по включению, со значениями в C. Рассмотрение систем путей со значениями в категории измеримых пространств позволяет прояснить многие аспекты классической теории Марковских процессов. Я опишу несколько основных способов построения таких систем путей по абстрактным математическим объектам, в частности, по счетным категориям. Одно из применений этих конструкций позволяет дать математически строгое и довольно элегантное построение динамических моделей, возникающих в популяционной генетике.

Google-translate renders that as "A system of paths on a time interval T with a value in the category C is a contravariant functor on the category of sub-intervals in T ordered by inclusion with values ​​in C. Consideration of systems of paths with values ​​in the category of measurable spaces makes it possible to clarify many aspects of the classical theory of Markov processes. I will describe several basic ways of constructing such systems of paths on abstract mathematical objects, in particular, in countable categories. One of the applications of these constructions allows us to give a mathematically rigorous and rather elegant construction of dynamic models emerging in population genetics."

[60] Notes on type systems, September 8, 2009. Unpublished. [ bib | files | pdf ]

A version of this paper was posted here.

[61] Pierre Deligne. Voevodsky's lectures on motivic cohomology 2000/2001. In Algebraic topology, volume 4 of Abel Symp., pages 355--409. Springer, Berlin, 2009. [ bib | DOI | earlier preprint | preprint | pdf | http ]

These lecture notes cover four topics. There is a proof of the fact that the functors represented by the motivic Eilenberg-Maclane spaces on the motivic homotopy category coincide with the motivic cohomology defined in terms of the motivic complexes. There is a description of the equivariant motivic homotopy category for a finite flat group scheme (over a noetherian base) together with a new characterization of 𝔸1-equivalences. There is a part where we introduce a class of sheaves called solid sheaves. Finally there is a part where we study functors of the form X ⟶ X/G and X ⟶ XW and show that they preserve equivalences between term-wise ind-solid simplicial sheaves.

[62] Vladimir Voevodsky. Bloch-kato conjecture. 2010. [ bib | files | pdf ]
This brief unpublished note is a careful statement in elementary language of (part of) the Bloch-Kato conjecture.
[63] Vladimir Voevodsky. Homotopy theory of simplicial sheaves in completely decomposable topologies. J. Pure Appl. Algebra, 214(8):1384--1398, 2010. [ bib | DOI | earlier preprint | preprint | MR | pdf ]

There are two approaches to the homotopy theory of simplicial (pre-)sheaves. One developed by Joyal and Jardine works for all sites but produces a model structure which is not finitely generated even in the case of sheaves on a Noetherian topological space. The other one developed by Brown and Gersten gives a nice model structure for sheaves on a Noetherian space of finite dimension but does not extend to all sites. In this paper we define a class of sites for which a generalized version of the Brown–Gersten approach works.

[64] Vladimir Voevodsky. Unstable motivic homotopy categories in Nisnevich and cdh-topologies. J. Pure Appl. Algebra, 214(8):1399--1406, 2010. [ bib | DOI | earlier preprint | preprint | MR | pdf ]

The motivic homotopy categories can be defined with respect to different topologies and different underlying categories of schemes. For a number of reasons (mainly because of the Gluing Theorem) the motivic homotopy category of smooth schemes with respect to the Nisnevich topology plays a distinguished role but in some cases it is desirable to be able to work with all schemes instead of the smooth ones. In this paper we prove that, under the resolution of singularities assumption, the unstable motivic homotopy category of all schemes over a field with respect to the cdh-topology is almost equivalent to the unstable motivic homotopy category of smooth schemes over the same field with respect to the Nisnevich topology.

[65] Vladimir Voevodsky. Motives over simplicial schemes. J. K-Theory, 5(1):1--38, 2010. [ bib | DOI | earlier preprint | preprint | MR | pdf ]

In this paper we define the triangulated category of motives over a simplicial scheme. The morphisms between the Tate objects in this category compute the motivic cohomology of the underlying scheme. In the last section we consider the special case of "embedded" simplicial schemes, which correspond to the subsheaves of the constant sheaf and naturally appear in the descent problems for motivic cohomology such as the Bloch-Kato conjecture.

[66] Vladimir Voevodsky. Simplicial radditive functors. J. K-Theory, 5(2):201--244, 2010. [ bib | DOI | earlier preprint | preprint | MR | pdf ]

The simplicial extension of any functor from Sets to Sets which commutes with directed colimits takes weak equivalences to weak equivalences. The goal of the present paper is construct a framework which can be used to proof results of this kind for a wide class of closed model categories and functors between those categories.

[67] Vladimir Voevodsky. Motivic Eilenberg-Maclane spaces. Publ. Math. Inst. Hautes Études Sci., (112):1--99, 2010. [ bib | DOI | earlier preprint | preprint | MR | pdf ]

This paper is the second one in a series of papers about operations in motivic cohomology. Here we show that in the context of smooth schemes over a field of characteristic zero all the bi-stable operations can be obtained in the usual way from the motivic reduced powers and the Bockstein homomorphism.

[68] Vladimir Voevodsky. Cancellation theorem. Doc. Math., pages 671--685, 2010. Special volume: Andrei A. Suslin's sixtieth birthday. [ bib | earlier preprint | preprint | MR | pdf | .html ]

In this paper we give a direct proof of the fact that for any schemes of finite type X, Y over a Noetherian scheme S the natural map of presheaves with transfers Hom(ℤtr(X), ℤtr(Y)) → Hom(ℤtr(X) ⊗tr 𝔾m, ℤtr(Y) ⊗tr 𝔾m) is a (weak) 𝔸1-homotopy equivalence. As a corollary we deduce that the Tate motive is quasi-invertible in the triangulated categories of motives over perfect fields.

[69] Vladimir Voevodsky. On motivic cohomology with ℤ/l-coefficients. Ann. of Math. (2), 174(1):401--438, 2011. [ bib | DOI | earlier preprint | preprint | MR | pdf ]

In this paper we prove the conjecture of Bloch and Kato which relates Milnor's K-theory of a field with its Galois cohomology as well as the related comparisons results for motivic cohomology with finite coefficients in the Nisnevich and étale topologies.

[70] Vladimir Voevodsky. Univalent foundations project. October, 2010. 12 pages. [ bib | .pdf ]

This note is a modified version of an NSF grant application. In it Voevodsky sketches his insights into univalent foundations, how he came to them, his plan for showing soundness, and his conjecture about computability of univalence. He finishes with some code from Foundations and some references.

[71] Formal Languages, partial algebraic theories and homotopy category -- Формальные языки, частичные алгебраические теории и гомотопическая категория (in English), June 27, 2010. A talk at Algebraic Geometry, K-theory, and Motives (a conference dedicated to Andrei Suslin's 60th birthday). [ bib | video ]
[72] Vladimir Voevodsky. Foundations: Development of the univalent foundations of mathematics in Coq. 2010. A Coq library of formalized proofs. [ bib | http ]

Voevodsky's original development of the univalent foundations of mathematics in Coq.

[73] Vladimir Voevodsky. Univalent foundations. In Mini-Workshop: The Homotopy Interpretation of Constructive Type Theory, pages 7--10. Mathematisches Forschungsinstitut Oberwolfach, February 27 - March 5, 2011. [ bib | DOI | pdf ]

This series of lectures was an introduction to "univalent foundations" — a new foundational system for mathematics based on type theory and homotopy theory — touching on their overall philosophy, some of the challenges involved in developing mathematics in these foundations, and the question of their consistency relative to the standard foundations.

[74] Унивалентные основания математики -- Univalent foundations of mathematics (in Russian), June 7, 2011. A talk in the Seminar of the Department of Algebra. [ bib | http ]
[75] Vladimir Voevodsky. Resizing Rules - their use and semantic justification. September 11, 2011. Slides from a talk in Bergen. [ bib | pdf ]
[76] Унивалентные Основания Математики -- Univalent foundations of mathematics (in Russian), December 29, 2011. A talk at a one-day conference dedicated to the memory of V. A. Iskovskikh, Moscow, Steklov Mathematical Institute. [ bib | video ]
[77] Chris Kapulkin, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. Univalence in simplicial sets. March, 2012. [ bib | preprint ]

The Simplicial Model of Univalent Foundations, below, is an expanded version of this paper, presenting the logical as well as the simplicial aspects of the model.

[78] Chris Kapulkin and Peter LeFanu Lumsdaine. The Simplicial Model of Univalent Foundations (after Voevodsky). November, 2012. [ bib | preprint ]

In this largely expository paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we first give a new technique for constructing models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan fibration, and use it to exhibit a model in simplicial sets. Lastly, we introduce the Univalence Axiom, in several equivalent formulations, and show that it holds in this model. As a corollary, we conclude that Univalent Foundations are at least as consistent as ZFC with two inaccessible cardinals [provided the Initiality Conjecture of Voevodsky is true].

The main results of the paper are due to Vladimir Voevodsky. He was originally a co-author, but withdrew, in order to prepare a research paper on the result in his own style.

[79] Vladimir Voevodsky. A test type system, March 5, 2013. An unfinished unreleased manuscript. [ bib | files | pdf ]

This note gives some ideas about the test type system TTS with secondary witnessed which Dan Grayson and I have been working on implementing. While TTS by itself has (most likely) decidable definitional equality and typing making secondary witnesses to be formally speaking unnecessary, they become essential for the implementation of more complex systems with undecidable typing such as HTS.

[80] Univalent Foundations of Mathematics, July 25, 2013. A talk at the University of Coimbra. [ bib | http ]

I will outline the main ideas of the new approach to foundations of practical mathematics which we call univalent foundations. Mathematical objects and their equivalences form sets, groupoids or higher groupoids. According to Grothendieck's idea higher groupoids are the same as homotopy types. Therefore mathematics may be considered as studying homotopy types and structures on them. Homotopy type theories, the underlying formal deduction system of the univalent foundations allows one to reason about such objects directly.

[81] Vladimir Voevodsky. The equivalence axiom and univalent models of type theory. (Talk at CMU on February 4, 2010). February, 2014. [ bib | preprint | files | pdf ]

This is the text of my talk at CMU on Feb. 4, 2010 where I gave the second public presentation of the Univalence Axiom (called "equivalence axiom" in the text). The first presentation of the axiom was in a lecture at LMU Munich in November 2009.


Voevodsky wanted to publish this, so it is being arranged.

[82] Vladimir Voevodsky, Benedikt Ahrens, Daniel R. Grayson, et al. UniMath - a computer-checked library of univalent mathematics. March, 2014. [ bib | http ]

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

[83] Vladimir Voevodsky. Univalent foundations - new type-theoretic foundations of mathematics. April 22, 2014. Slides from a talk at IHP, Paris. [ bib | pdf ]
[84] A simple type system with two identity types, May 11, 2014. An unfinished unreleased (?) manuscript. [ bib | files | pdf ]

We call this system and its further extensions HTS for "homotopy type system". It is an extension of the Martin-Löf type system with some additional constructs which reflect the structures which exist in the target of the canonical univalent model of the Martin-Löf system.


Its sequel is HTS (II).

[85] HTS (II), May 11, 2014. An unfinished unreleased (?) manuscript. [ bib | files | pdf ]

This brief note is a continuation of A simple type system with two identity types.

[86] Vladimir Voevodsky. The origins and motivations of Univalent Foundations. The Institute Letter, Summer, 2014. [ bib | http ]
[87] Vladimir Voevodsky. C-system of a module over a monad on sets. July, 2014. [ bib | preprint | files ]

This is the second paper in a series, starting with Subsystems and regular quotients of C-systems, that aims to provide mathematical descriptions of objects and constructions related to the first few steps of the semantical theory of dependent type systems.

We construct for any pair (R,LM), where R is a monad on sets and LM is a left module over R, a C-system (contextual category) CC(R,LM) and describe a class of sub-quotients of CC(R,LM) in terms of objects directly constructed from R and LM. In the special case of the monads of expressions associated with nominal signatures this construction gives the C-systems of general dependent type theories when they are specified by collections of judgements of the four standard kinds.


This paper was submitted for publication, but after the first referee's report, it evolved into C-system of a module over a Jf-relative monad and will not be published separately.

[88] Как писать математику используя систему Кок I -- How to write mathematics in the Coq system, I (in Russian), July 29, 2014. A talk in the Summer mathematical school on Algebra and Geometry, Yaroslavl, July 25-31, 2014, Летняя математическая школа "Алгебра и геометрия". [ bib | video | .html ]

Кок - это программа, которая предоставляет набор инструментов для эффективной работы с формальными рассуждениями в современной (зависимой, полиморфной) теории типов. На основании таких теорий типов сформулированы унивалентные основания, в которых примитивными объектами являются не множества, а бесконечность-групойды или, эквивалентно, гомотопические типы. Поэтому, используя Кок, можно "писать" унивалентную математику в такой форме, что правильность рассуждений проверяется компьютером. Я покажу часть имеющейся у нас сейчас библиотеки конструкций, включая конструкцию локализации коммутативных колец, и мы попробуем в классе построить конструкцию спектров коммутативных колец. Студентам будет полезно посмотреть статью Experimental library of univalent formalization of mathematics, а также скачать и установить программу Кок.

Google-translate renders that as: Coq is a program that provides a set of tools for effective work with formal reasoning in the modern (dependent, polymorphic) theory of types. On the basis of such theories of types, univalent bases are formulated in which primitive objects are not sets, but infinity-groupoids or, equivalently, homotopy types. Therefore, using Coq, one can "write" univalent mathematics in such a way that the correctness of reasoning is checked by a computer. I will show some of the library of constructions that we have now, including the construction of the localization of commutative rings, and we will try to present a construction of the spectrum of a commutative ring. It will be useful for students to see the article "An experimental library of univalent formalization of mathematics", as well as to download and install the Coq program.

[89] Как писать математику используя систему Кок II -- How to write mathematics in the Coq system, II (in Russian), July 30, 2014. A talk in the Summer mathematical school on Algebra and Geometry, Yaroslavl, July 25-31, 2014, Летняя математическая школа "Алгебра и геометрия". [ bib | video | .html ]
[90] Vladimir Voevodsky. B-systems. October, 2014. [ bib | preprint | files | pdf ]

B-systems are algebras (models) of an essentially algebraic theory that is expected to be constructively equivalent to the essentially algebraic theory of C-systems which is, in turn, constructively equivalent to the theory of contextual categories. The theory of B-systems is closer in its form to the structures directly modeled by contexts and typing judgements of (dependent) type theories and further away from categories than contextual categories and C-systems.


Voevodsky submitted this paper for publication, but then, in November, 2015, withdrew it. We don't know why, but he is said to have considered it still "very patchy".

See also B-presheaves, which is perhaps related.

[91] B-presheaves, October, 2014. An unfinished unreleased manuscript. [ bib | files | pdf ]

[92] Vladimir Voevodsky. A universe polymorphic type system, October 22, 2014. An unfinished unreleased manuscript. [ bib | files | pdf ]

These notes present a detailed description of the type theory with universe polymorphism (UPTS), possibly the one Voevodsky preferred for formalization and for semantic proofs.


Voevodsky posted this document here, on wikispaces.com. That web site is due to shut down July 31, 2018.

[93] Vladimir Voevodsky. Products of families of types in the C-systems defined by a universe category. March, 2015. [ bib | preprint ]

We introduce the notion of a (∏,λ)-structure on a C-system and show that C-systems with (∏,λ)-structures are constructively equivalent to contextual categories with products of families of types. We then show how to construct (∏,λ)-structures on C-systems of the form CC(C,p) defined by a universe p in a locally Cartesian closed category C from a simple pull-back square based on p. In the last section we prove a theorem that asserts that our construction is functorial.

This preprint evolved into three published papers:

  1. Products of families of types and (∏,λ)-structures on C-systems
  2. C-systems defined by universe categories: presheaves
  3. The (∏,λ)-structures on the {C}-systems defined by universe categories
[94] Vladimir Voevodsky. Martin-Löf identity types in the C-systems defined by a universe category. May, 2015. Submitted, 51 pages. [ bib | preprint ]

This paper continues the series of papers that develop a new approach to syntax and semantics of dependent type theories. Here we study the interpretation of the rules of the identity types in the intensional Martin-Löf type theories on the C-systems that arise from universe categories. In the first part of the paper we develop constructions that produce interpretations of these rules from certain structures on universe categories while in the second we study the functoriality of these constructions with respect to functors of universe categories. The results of the first part of the paper play a crucial role in the construction of the univalent model of type theory in simplicial sets.


Voevodsky submitted this paper for publication, and a referee's report has been received. There may be further work to do before it can be published.

[95] C-systems (in English), September 15, 2015. A talk in the Seminar of the Department of Algebra and of the Department of Algebraic Geometry (Shafarevich Seminar). [ bib | video ]

Type theories are formal deduction systems similar in function to the system of predicate logic. They can be used to formalize reasoning about various aspects of the world. C-systems appear as the central class of objects in the mathematical study of type theories. They are essentially algebraic structures, i.e., algebraic structures where some operations are defined only for arguments that themselves satisfy equations on more basic operations. I will explain what C-systems are and how they arise from syntax on the one hand and from mathematical categories such as simplicial sets on the other.

[96] Vladimir Voevodsky. Lawvere theories and C-systems. December, 2015. 15 pages. [ bib | preprint ]

In this paper we consider the class of l-bijective C-systems, i.e., C-systems for which the length function is a bijection. The main result of the paper is a construction of an isomorphism between two categories - the category of l-bijective C-systems and the category of Lawvere theories.


This paper will be published by Vladimir Voevodsky and Marcelo Fiore, and has been submitted for publication.

[97] Álvaro Pelayo, Vladimir Voevodsky, and Michael A. Warren. A univalent formalization of the p-adic numbers. Math. Structures Comput. Sci., 25(5):1147--1171, 2015. [ bib | DOI | preprint | MR | pdf ]

The goal of this paper is to report on a formalization of the p-adic numbers in the setting of the second author's univalent foundations program. This formalization, which has been verified in the Coq proof assistant, provides an approach to the p-adic numbers in constructive algebra and analysis.

[98] Vladimir Voevodsky. An experimental library of formalized mathematics based on the univalent foundations. Math. Structures Comput. Sci., 25(5):1278--1294, 2015. [ bib | DOI | preprint | MR | pdf ]

This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Univalence in Simplicial Sets).

[99] Vladimir Voevodsky. A C-system defined by a universe category. Theory Appl. Categ., 30:Paper No. 37, 1181--1215, 2015. [ bib | preprint | MR | pdf | .html ]

This is the third paper in a series, starting with Subsystems and regular quotients of C-systems. In it we construct a C-system CC(C,p) starting from a category C together with a morphism p : tilde-U → U, a choice of pull-back squares based on p for all morphisms to U and a choice of a final object of C. Such a quadruple is called a universe category. We then define universe category functors and construct homomorphisms of C-systems CC(C,p) defined by universe category functors.

In the last section we give, for any C-system CC, three different constructions of pairs ((C,p),H) where (C,p) is a universe category and H : CC → CC(C,p) is an isomorphism.

[100] Vladimir Voevodsky. Lawvere theories and Jf-relative monads. January, 2016. 21 pages. [ bib | preprint | files ]

In this paper we provide a detailed construction of an equivalence between the category of Lawvere theories and the category of relative monads on the obvious functor Jf : F → Sets where F is the category with the set of objects ℕ and morphisms being the functions between the standard finite sets of the corresponding cardinalities. The methods of this paper are fully constructive and it should be formalizable in the Zermelo-Fraenkel theory without the axiom of choice and the excluded middle. It is also easily formalizable in the UniMath.

[101] Vladimir Voevodsky. C-system of a module over a Jf-relative monad. February, 2016. Submitted for publication. [ bib | preprint | files ]

Let F be the category with the set of objects ℕ and morphisms being the functions between the standard finite sets of the corresponding cardinalities. Let Jf : F → Sets be the obvious functor from this category to the category of sets. In this paper we construct, for any relative monad RR on Jf and a left module LM over RR, a C-system C(RR,LM) and explicitly compute the action of the B-system operations on its B-sets.

In the following paper it is used to provide a rigorous mathematical approach to the construction of the C-systems underlying the term models of a wide class of dependent type theories.

This paper is a result of evolution of C-system of a module over a monad on sets. However this paper is much more detailed and contains a lot of material that is not contained in that one. It also does not cover some material that is covered in that one.


Voevodsky's most recent draft is dated May 25, 2017, and has grown to 61 pages, in response to the second referee's report. Grayson is editing the paper to prepare it for publication.

[102] Mathematical theory of type theories and the initiality conjecture, April, 2016. Research proposal to the Templeton Foundation for 2016-2019, project description. [ bib | pdf ]
[103] Vladimir Voevodsky. Products of families of types and (∏,λ)-structures on C-systems. Theory Appl. Categ., 31:Paper No. 36, 1044--1094, 2016. [ bib | preprint | MR | pdf | ZB | .html ]

The first part of the paper adds to the general theory of C-systems and may be used as an advanced introduction to C-systems.

This paper is the first of the three papers into which the preprint Products of families of types in the C-systems defined by a universe category evolved during publication.

[104] Vladimir Voevodsky. Subsystems and regular quotients of C-systems. In A panorama of mathematics: pure and applied, volume 658 of Contemp. Math., pages 127--137. Amer. Math. Soc., Providence, RI, 2016. [ bib | DOI | preprint | MR ]

C-systems were introduced by J. Cartmell under the name "contextual categories". In this note we study sub-objects and quotient-objects of C-systems. In the case of the sub-objects we consider all sub-objects while in the case of the quotient-objects only {\em regular} quotients that in particular have the property that the corresponding projection morphism is surjective both on objects and on morphisms. It is one of several short papers based on the material of the Notes on Type Systems by the same author.


This paper has two sequels, forming a series of three papers:

[105] Vladimir Voevodsky. C-systems defined by universe categories: presheaves. Theory Appl. Categ., 32:Paper No. 3, 53--112, 2017. [ bib | preprint | MR | pdf | ZB | .html ]

The paper introduces and studies "canonical" presheaves on C-systems defined by universe categories. It is the second of the three papers into which the preprint Products of families of types in the C-systems defined by a universe category evolved during publication.

This paper was written to present the constructions that were originally introduced for the proof of functoriality of (∏,λ) structures obtained from the (P,tilde-P) structures. In the process of writing up this proof it became clear that the main objects required for it -- the "almost representations" μn and tilde-μn of the presheaves Obn and tilde-Obn on the C-systems defined by locally Cartesian closed universe categories with binary product structures and the lemmas describing the behavior of these "almost representations" with respect to the universe category functors, play important role in the general theory that is quite independent from the analysis of the ∏,λ,β,η system of inference rules. This led to the decision to present these constructions together with the important intermediate ones such as Sig and Dp in a separate paper.

[106] Unimath - its present and its future, July 10, 2017. Video and slides of a talk, Isaac Newton Institute for Mathematical Sciences, Cambridge. [ bib | slides | video ]

UniMath refers to several things. It is a univalent foundation of mathematics. It is the subset of Coq in which this foundation is currently implemented and it is a library of formalized mathematics written using this implementation. My talk will be mostly about the library. I will give examples of problems whose constructions have been recently formalized in the UniMath as study problems by graduate students. I will give an example of a more complex problem whose construction has been recently formalized as a part of a paper accepted to a conference proceedings. Finally, I will outline a direction for the future development of the UniMath that requires constructions to considerably more complex problems that can only be stated in the univalent type theory and, as far as I know, have never been solved either formally or informally.


Toward the end of the talk, Voevodsky says it would be good to find a constructive proof to replace the "Merkurjev-Suslin transfinite argument" in the proof of Bloch-Kato. Merkurjev says they did not use any transfinite induction in their argument, and has provided the following additional details: "Let F be a field, S the set of all n-symbols over F (modulo l) and T the set of all finite subsets of S. We order T by inclusion. For any A in T let X_A be the product of norm varieties X_a for all symbols a in A. If A is a subset of a finite set B in T, we have projection X_B -> X_A and hence a field homomorphism F(X_A) -> F(X_B). Let F_1 be the colimit of this system of fields. Then construct a field extension F_2/F_1 the same way (replacing F by F1), etc. We get a tower of field extensions F in F_1 in F_2 in ... Finally, let K be the union of all F_i. Clearly, every n-symbol over K is trivial modulo l." See also Theorem 1.12 of the book The Norm Residue Theorem in Motivic Cohomology by Haesemeyer and Weibel, which presents a transfinite version of the argument.

[107] Simplicial and cubical sets, I -- how they relate to each other (joint work with Chris Kapulkin), July 27, 2017. Video of a talk, Isaac Newton Institute for Mathematical Sciences, Cambridge. [ bib | video ]

This talk covers the material in the paper Cubical approach to straightening.

[108] Simplicial and cubical sets, II -- the coherent nerve of a cubical category (joint work with K Kapulkin), August 3, 2017. Video of a talk, Isaac Newton Institute for Mathematical Sciences, Cambridge. [ bib | video ]

This talk covers the material in the paper Cubical approach to straightening.

[109] Models, Interpretations and the Initiality Conjectures, August 18, 2017. A talk the Special session on category theory and type theory in honor of Per Martin-Löf on his 75th birthday, August 17–19, 2017, during the Logic Colloquium 2017, August 14-20, in Stockholm. [ bib | files | pdf | http ]

Work on proving consistency of the intensional Martin-Löf type theory with a sequence of univalent universes ("MLTT+UA") led to the understanding that in type theory we do not know how to construct an interpretation of syntax from a model of inference rules. That is, we now have the concept of a model of inference rules and the concept of an interpretation of the syntax and a conjecture that implies that the former always defines the latter. This conjecture, stated as the statement that the term model is an initial object in the category of all models of a given kind, is called the Initiality Conjecture. In my talk I will outline the various parts of this new vision of the theory of syntax and semantics of dependent type theories.


This is a clear and enlightening sketch of Voevodsky's entire program!

[110] Vladimir Voevodsky. The (∏,λ)-structures on the C-systems defined by universe categories. Theory Appl. Categ., 32:Paper No. 4, 113--121, 2017. [ bib | preprint | MR | pdf | ZB | .html ]

This is the third of the three papers into which the preprint Products of families of types on the C-systems defined by a universe category evolved during publication.

We define the notion of a (P,tilde-P)-structure on a universe p in a locally Cartesian closed category category with a binary product structure and construct a (∏,λ)-structure on the C-systems CC(C,p) from a (P,tilde-P)-structure on p. We then define homomorphisms of C-systems with (∏,λ)-structures and functors of universe categories with (P,tilde-P)-structures and show that our construction is functorial relative to these definitions. The proofs in this paper rely on the general constructions of the previous paper "C-systems defined by universe categories: presheaves".

[111] Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. Categorical Structures for Type Theory in Univalent Foundations. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of Leibniz International Proceedings in Informatics (LIPIcs), pages 8:1--8:16, Dagstuhl, Germany, 2017. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [ bib | DOI | preprint | files | MR | pdf | http ]

In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in the setting of univalent foundations, where the relationships between them can be stated more transparently. Specifically, we construct maps between the different structures and show that these maps are equivalences under suitable assumptions.

We then analyze how these structures transfer along (weak and strong) equivalences of categories, and, in particular, show how they descend from a category (not assumed univalent/saturated) to its Rezk completion. To this end, we introduce relative universes, generalizing the preceding notions, and study the transfer of such relative universes along suitable structure.

We work throughout in (intensional) dependent type theory; some results, but not all, assume the univalence axiom. All the material of this paper has been formalized in Coq, over the UniMath library.

[112] Benedikt Ahrens, Peter LeFanu Lumsdaine, and Vladimir Voevodsky. Categorical Structures for Type Theory in Univalent Foundations. Logical Methods in Computer Science, 14, issue 3, September 11, 2018. [ bib | pdf | http ]

This paper is essentially the same as the one above of the same title, which appeared in proceedings of a conference.

[113] Krzysztof Kapulkin and Vladimir Voevodsky. Cubical approach to straightening. 2018. [ bib | preprint ]

For a suitable choice of the cube category, we construct a topology on it such that sheaves with respect to this topology are exactly simplicial sets (thus establishing simplicial sets as a subcategory of the category of cubical sets). We then generalize the construction of the homotopy coherent nerve to cubical categories and establish an analog of Lurie’s straightening–unstraightening construction.

Earlier titles for this paper were "Simplicial Nerve of a Cubical Category" and "The nerve of a cubical category and the Grothendieck construction".

[114] Christian Haesemeyer and Charles A. Weibel. The Norm Residue Theorem in Motivic Cohomology. June 27, 2018. [ bib | .pdf ]

This book by Haesemeyer and Weibel presents a proof of the Bloch-Kato and Beilinson-Lichtenbaum conjectures.


This file was generated by a locally modified version of bibtex2html 1.98.

Valid HTML 4.01 StrictValid CSS!