[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):265268, 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.
Piecewise 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 handwritten 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)):183184, 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.32.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 VoevodskyKapranov 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 199227. 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):11551167, 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 ncategory generated by a cube, oriented matroids and
higher Bruhat orders.
Funktsional. Anal. i Prilozhen., 25(1):6265, 1991.
[ bib 
DOI 
MR 
Russian pdf 
pdf 
http ]
In investigating multidimensional generalizations of the YangBaxter 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
S_{n} 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 S_{n} in ℝ^{n}. In the present note we
give an interpretation of B(n,k) as the sets of some kdimensional strips in
an ndimensional cube. This permits us to clarify the abovementioned
connections, in particular to prove a hypothesis from their papers and disprove
another hypothesis of theirs.

[11]

M. M. Kapranov and V. A. Voevodsky.
Combinatorialgeometric aspects of polycategory theory: pasting
schemes and higher Bruhat orders (list of results).
Cahiers Topologie Géom. Différentielle Catég.,
32(1):1127, 1991.
International Category Theory Meeting (Bangor, 1989 and Cambridge,
1990).
[ bib 
MR 
pdf 
http ]
This talk is devoted to detailed study of free ncategories and
their relations with more "classical"
geometric objects. Among these objects we list convex polytopes,
their triangulations, configurations of hyperplanes, oriented
matroids, and socalled "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
ncategories 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):2946, 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.32.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 VoevodskyKapranov approach.

[13]

V. A. Voevodskiĭ.
Galois groups of function fields over fields of finite type over ℚ.
Uspekhi Mat. Nauk, 46(5(281)):163164, 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):13311342, 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 crossreferences are broken and print as question marks. We would like to find a digital version.

[17]

M. Kapranov and V. Voevodsky.
Braided monoidal 2categories and ManinSchechtman higher
braid groups.
J. Pure Appl. Algebra, 92(3):241267, 1994.
[ bib 
DOI 
MR 
pdf ]
We study a certain coherence problem for braided monoidal 2categories. 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 A_{1} ⊗ ··· ⊗ A_{n}. It turns out that in the 2categorical case we have to consider the socalled higher braid group T(2,n) introduced by Manin and Schechtman. The main result is that T(2,n) naturally acts by 2automorphisms on the canonical 1morphism A_{1} ⊗ ··· ⊗ A_{n} → A_{n} ⊗ ··· ⊗ A_{1} for any objects A_{1}, ..., A_{n}.

[18]

M. M. Kapranov and V. A. Voevodsky.
2categories and Zamolodchikov tetrahedra equations.
In Algebraic groups and their generalizations: quantum and
infinitedimensional methods (University Park, PA, 1991), volume 56 of
Proc. Sympos. Pure Math., pages 177259. 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):187198, 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 zerocycles of selfproducts of varieties, in the book
"Moduli of vector bundles (Sanda, 1994; Kyoto, 1994)", 265285, 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):6194, 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):111153, 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 semisimple Qlinear 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 BlochKato conjecture in the étale cohomology, the QuiltenLichtenbaum conjecture and the BeilinsonSoulé vanishing conjecture in the algebraic Ktheory, 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
579604, 1998.
[ bib 
MR 
pdf 
.html ]

[24]

V. Voevodsky.
Voevodsky's Seattle lectures: Ktheory and motivic cohomology.
In Algebraic Ktheory (Seattle, WA, 1997), volume 67 of
Proc. Sympos. Pure Math., pages 283303. 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 Ktheory, 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):45143 (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 cdhtopology, 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 cdhtopology on the categories of schemes over a base.

[28]

Andrei Suslin and Vladimir Voevodsky.
BlochKato 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
117189. 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 BlochKato conjecture which asserts that the cotorsion in Milnor's Kgroups of a field is isomorphic to its etale cohomology and the BeilinsonLichtenbaum conjecture which provides a complete description of the motivic cohomology with finite coefficients in terms of the etale cohomology. Since the BlochKato conjecture is known in dimension 2 (and in dimension 3 for ℤ/2coefficients) we obtain in particular a proof of the BeilinsonLichtenbaum conjecture in weight 2 and in weight 3 for ℤ/2coefficients.

[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 39. 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 1086. 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 cdhtopology. 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 87137. 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 Kcohomology, 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 MayerVietoris 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 138187. 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 MayerVietories 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, BorelMoore 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 188238. 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 Homgroups 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 2torsion in motivic cohomology.
July, 2001.
[ bib 
preprint ]
In this paper we prove the 2local part of the BeilinsonLichtenbaum conjectures on tosion in motivic cohomology. In particular we prove the Milnor conjecture relating Milnor's Ktheory and the Galois cohomology with ℤ/2coefficients. 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 ℤ/2coefficients".

[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 Ktheory 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):351355, 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 Ktheory.
In Recent progress in homotopy theory (Baltimore, MD,
2000), volume 293 of Contemp. Math., pages 371379. Amer. Math. Soc.,
Providence, RI, 2002.
[ bib 
DOI 
preprint 
MR 
pdf ]
We describe a simple construction of the spectral sequence relating algebraic Ktheory 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 EilenbergMaclane spectrum H_{ℤ}. The second is the motivic analog of the fact that the functor Ω^{1}Σ^{1} takes nconnected spaces to nconnected 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
334. 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):157, 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 ℤ/2coefficients.
Publ. Math. Inst. Hautes Études Sci., (98):59104, 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:106115, 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 EilenbergMaclane spectrum. As a corollary one concludes that the slices of any spectrum are modules over the motivic EilenbergMacLane spectrum. To prove our result we analyze the unstable homotopy type of the symmetric powers of the Tsphere.

[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 nonrecombinant 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 nonrecombinant 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 ZermeloFraenkel theory became generally accepted. Contemporary constructions
and proofs can not be translated in any sensible way into the ZermeloFraenkel theory. One can (may be!) translate the categorical definition of group cohomology into the ZFtheory 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 K^{M}_{*}/2 with applications to quadratic
forms.
Ann. of Math. (2), 165(1):113, 2007.
[ bib 
DOI 
earlier preprint 
preprint 
MR 
pdf ]
We construct a fourterm exact sequence which provides information on the kernel and cokernel of the multiplication by a pure symbol in Milnor's Ktheory 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 KhanRostSujatha conjecture and the Jfiltration 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. SpringerVerlag, 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 147221.
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 preprocess.

[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 году, понял, что то, что я придумывал, бесполезно. В моей жизни, пока, это была, пожалуй, самая большая научная неудача. Очень много работы было вложено в проект, который полностью провалился. Какаято польза, конечно, всетаки, была  я выучил много из теории вероятности, которую знал плохо, а также узнал много нового про демографию и демографическую историю."
Googletranslate 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. Рассмотрение систем путей со значениями в категории измеримых пространств позволяет прояснить многие аспекты классической теории Марковских процессов. Я опишу несколько основных способов построения таких систем путей по абстрактным математическим объектам, в частности, по счетным категориям. Одно из применений этих конструкций позволяет дать математически строгое и довольно элегантное построение динамических моделей, возникающих в популяционной генетике.
Googletranslate 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 subintervals 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
355409. 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 EilenbergMaclane 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 ⟶ X^{W} and show that they preserve equivalences between termwise indsolid simplicial sheaves.

[62]

Vladimir Voevodsky.
Blochkato conjecture.
2010.
[ bib 
files 
pdf ]
This brief unpublished note is a careful statement in elementary language of (part of) the BlochKato conjecture.

[63]

Vladimir Voevodsky.
Homotopy theory of simplicial sheaves in completely decomposable
topologies.
J. Pure Appl. Algebra, 214(8):13841398, 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
cdhtopologies.
J. Pure Appl. Algebra, 214(8):13991406, 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 cdhtopology 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. KTheory, 5(1):138, 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 BlochKato conjecture.

[66]

Vladimir Voevodsky.
Simplicial radditive functors.
J. KTheory, 5(2):201244, 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 EilenbergMaclane spaces.
Publ. Math. Inst. Hautes Études Sci., (112):199, 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 bistable 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 671685, 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 quasiinvertible in the triangulated categories of motives over perfect fields.

[69]

Vladimir Voevodsky.
On motivic cohomology with ℤ/lcoefficients.
Ann. of Math. (2), 174(1):401438, 2011.
[ bib 
DOI 
earlier preprint 
preprint 
MR 
pdf ]
In this paper we prove the conjecture of Bloch and Kato which relates Milnor's Ktheory 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, Ktheory, 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 MiniWorkshop: The Homotopy Interpretation of Constructive
Type Theory, pages 710. 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 oneday 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 coauthor, 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 computerchecked 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 typetheoretic 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 MartinLöf type system with some additional constructs which reflect the structures which exist in the target of the canonical univalent model of the MartinLö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.
Csystem 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 Csystems, 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 Csystem (contextual category) CC(R,LM) and describe a class of subquotients 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 Csystems 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 Csystem of a module over a Jfrelative 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 2531, 2014, Летняя математическая
школа "Алгебра и геометрия".
[ bib 
video 
.html ]
Кок  это программа, которая предоставляет набор инструментов для эффективной работы с формальными рассуждениями в современной (зависимой, полиморфной) теории типов.
На основании таких теорий типов сформулированы унивалентные основания, в которых примитивными объектами являются не множества, а бесконечностьгрупойды или, эквивалентно, гомотопические типы.
Поэтому, используя Кок, можно "писать" унивалентную математику в такой форме, что правильность рассуждений проверяется компьютером.
Я покажу часть имеющейся у нас сейчас библиотеки конструкций, включая конструкцию локализации коммутативных колец, и мы попробуем в классе построить конструкцию спектров коммутативных колец.
Студентам будет полезно посмотреть статью Experimental library of univalent formalization of mathematics, а также скачать и установить программу Кок.
Googletranslate 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 infinitygroupoids 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 2531, 2014, Летняя математическая
школа "Алгебра и геометрия".
[ bib 
video 
.html ]

[90]

Vladimir Voevodsky.
Bsystems.
October, 2014.
[ bib 
preprint 
files 
pdf ]
Bsystems are algebras (models) of an essentially algebraic theory that is expected to be constructively equivalent to the essentially algebraic theory of Csystems which is, in turn, constructively equivalent to the theory of contextual categories. The theory of Bsystems 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 Csystems.
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 Bpresheaves, which is perhaps related.

[91]

Bpresheaves, 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 Csystems defined by a
universe category.
March, 2015.
[ bib 
preprint ]
We introduce the notion of a (∏,λ)structure on a Csystem and show that Csystems with (∏,λ)structures are constructively equivalent to contextual categories with products of families of types. We then show how to construct (∏,λ)structures on Csystems of the form CC(C,p) defined by a universe p in a locally Cartesian closed category C from a simple pullback 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:
 Products of families of types and (∏,λ)structures on Csystems
 Csystems defined by universe categories: presheaves
 The (∏,λ)structures on the {C}systems defined by universe categories

[94]

Vladimir Voevodsky.
MartinLöf identity types in the Csystems 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 MartinLöf type theories on the Csystems 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]

Csystems (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. Csystems 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 Csystems 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 Csystems.
December, 2015.
15 pages.
[ bib 
preprint ]
In this paper we consider the class of lbijective Csystems, i.e., Csystems 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 lbijective Csystems 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 padic numbers.
Math. Structures Comput. Sci., 25(5):11471171, 2015.
[ bib 
DOI 
preprint 
MR 
pdf ]
The goal of this paper is to report on a formalization of the padic 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 padic 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):12781294, 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 Csystem defined by a universe category.
Theory Appl. Categ., 30:Paper No. 37, 11811215, 2015.
[ bib 
preprint 
MR 
pdf 
.html ]
This is the third paper in a series, starting with Subsystems and regular quotients of Csystems. In it we construct a Csystem CC(C,p) starting from a category C together with a morphism p : tildeU → U, a choice of pullback 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 Csystems CC(C,p) defined by universe category functors.
In the last section we give, for any Csystem 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 Jfrelative 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 ZermeloFraenkel theory without the axiom of choice and the excluded middle. It is also easily formalizable in the UniMath.

[101]

Vladimir Voevodsky.
Csystem of a module over a Jfrelative 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 Csystem C(RR,LM) and explicitly compute the action of the Bsystem operations on its Bsets.
In the following paper it is used to provide a rigorous mathematical approach to the construction of the Csystems underlying the term models of a wide class of dependent type theories.
This paper is a result of evolution of Csystem 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 20162019, project
description.
[ bib 
pdf ]

[103]

Vladimir Voevodsky.
Products of families of types and (∏,λ)structures on Csystems.
Theory Appl. Categ., 31:Paper No. 36, 10441094, 2016.
[ bib 
preprint 
MR 
pdf 
ZB 
.html ]
The first part of the paper adds to the general theory of Csystems and may be used as an advanced introduction to Csystems.
This paper is the first of the three papers into which the preprint Products of families of types in the Csystems defined by a universe category evolved during publication.

[104]

Vladimir Voevodsky.
Subsystems and regular quotients of Csystems.
In A panorama of mathematics: pure and applied, volume 658 of
Contemp. Math., pages 127137. Amer. Math. Soc., Providence, RI, 2016.
[ bib 
DOI 
preprint 
MR ]
Csystems were introduced by J. Cartmell under the name "contextual categories".
In this note we study subobjects and quotientobjects of Csystems.
In the case of the subobjects we consider all subobjects while in the case of the quotientobjects 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.
Csystems defined by universe categories: presheaves.
Theory Appl. Categ., 32:Paper No. 3, 53112, 2017.
[ bib 
preprint 
MR 
pdf 
ZB 
.html ]
The paper introduces and studies "canonical" presheaves on Csystems defined by universe categories. It is the second of the three papers into which the preprint Products of families of types in the Csystems 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,tildeP) 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 Ob_{n} and tildeOb_{n} on the Csystems 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 D_{p} 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 "MerkurjevSuslin transfinite argument" in the proof of BlochKato. 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 nsymbols 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 nsymbol 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 MartinLöf on his 75th birthday, August 17–19, 2017, during
the Logic Colloquium 2017, August 1420, in Stockholm.
[ bib 
files 
pdf 
http ]
Work on proving consistency of the intensional MartinLö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 Csystems defined by universe
categories.
Theory Appl. Categ., 32:Paper No. 4, 113121, 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 Csystems defined by a universe category evolved during publication.
We define the notion of a (P,tildeP)structure on a universe p in a locally Cartesian closed category category with a binary product structure and construct a (∏,λ)structure on the Csystems CC(C,p) from a (P,tildeP)structure on p. We then define homomorphisms of Csystems with (∏,λ)structures and functors of universe categories with (P,tildeP)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 "Csystems 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:18:16,
Dagstuhl, Germany, 2017. Schloss DagstuhlLeibnizZentrum 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 typecategories, 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 BlochKato and
BeilinsonLichtenbaum conjectures.
