Abstract This paper continues a 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 …
Abstract This paper continues a 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.
For a suitable choice of the cube category, we construct a Grothendieck topology on it such that sheaves with respect to this topology are exactly simplicial sets (thus establishing simplicial …
For a suitable choice of the cube category, we construct a Grothendieck topology on it such that sheaves with respect to this topology are exactly simplicial sets (thus establishing simplicial sets as a reflective subcategory of cubical sets). We then extend the construction of the homotopy coherent nerve to cubical categories and establish an analogue of Lurie's straightening–unstraightening construction.
In this paper we consider the class of $\ell$-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 …
In this paper we consider the class of $\ell$-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 $\ell$-bijective C-systems and the category of Lawvere theories.
The main result of this paper may be stated as a construction of almost representations for the canonical presheaves of object extensions of length n on the C-systems defined by …
The main result of this paper may be stated as a construction of almost representations for the canonical presheaves of object extensions of length n on the C-systems defined by locally cartesian closed universe categories with binary product structures and the study of the behavior of these almost representations with respect to the universe category functors.
In addition, we study a number of constructions on presheaves on C-systems and on universe categories that are used in the proofs of our main results, but are expected to have other applications as well.
In this paper we continue the study of the most important structures on C-systems, the structures that correspond, in the case of the syntactic C-systems, to the $(Pi,lambda,app,beta,eta)$-system of inference …
In this paper we continue the study of the most important structures on C-systems, the structures that correspond, in the case of the syntactic C-systems, to the $(Pi,lambda,app,beta,eta)$-system of inference rules. One such structure was introduced by J. Cartmell and later studied by T. Streicher under the name of the products of families of types. We introduce the notion of a (Pi,lambda)-structure and construct a bijection, for a given C-system, between the set of (Pi,lambda)-structures and the set of Cartmell-Streicher structures. In the following paper we will show how to construct, and in some cases fully classify, the (Pi,λ)-structures on the C-systems that correspond to universe categories. The first section of the paper provides careful proofs of many of the properties of general C-systems. Methods of the paper are fully constructive, that is, neither the axiom of excluded middle nor the axiom of choice are used.
We define the notion of a (P,P-tilde)-structure on a universe p in a locally cartesian closed category category C with a binary product structure and construct a (Pi,lambda)-structure on the …
We define the notion of a (P,P-tilde)-structure on a universe p in a locally cartesian closed category category C with a binary product structure and construct a (Pi,lambda)-structure on the C-systems CC(C,p) from a (P,P-tilde)-structure on p. We then define homomorphisms of C-systems with (Pi,lambda)-structures and functors of universe categories with (P,P-tilde)-structures and show that our construction is functorial relative to these definitions.
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 …
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 univalent type theory, where the comparisons between them can be given more elementarily than in set-theoretic foundations. Specifically, we construct maps between the various types of structures, and show that assuming the Univalence axiom, some of the comparisons are equivalences. 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.
The main result of this paper may be stated as a construction of "almost representations" for the canonical presheaves of object extensions of length n on the C-systems defined by …
The main result of this paper may be stated as a construction of "almost representations" for the canonical presheaves of object extensions of length n on the C-systems defined by locally cartesian closed universe categories with binary product structures and the study of the behavior of these "almost representations" with respect to the universe category functors. In addition, we study a number of constructions on presheaves on C-systems and on universe categories that are used in the proofs of our main results, but are expected to have other applications as well.
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\rightarrow Sets$ where …
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\rightarrow Sets$ where $F$ is the category with the set of objects ${\bf N}$ 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.
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 …
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 version is essentially identical with the version published in Contemporary Mathematics n.658.
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\rightarrow Sets$ where …
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\rightarrow Sets$ where $F$ is the category with the set of objects ${\bf N}$ 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.
Let $F$ be the category with the set of objects $\bf N$ and morphisms being the functions between the standard finite sets of the corresponding cardinalities. Let $Jf:F\rightarrow Sets$ be …
Let $F$ be the category with the set of objects $\bf N$ and morphisms being the functions between the standard finite sets of the corresponding cardinalities. Let $Jf:F\rightarrow Sets$ be the obvious functor from this category to the category of sets. In this paper we construct, for any relative monad $\bf RR$ on $Jf$ and a left module $\bf LM$ over $\bf RR$, a C-system $C({\bf RR},{\bf 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 arXiv:1407.3394. However this paper is much more detailed and contains a lot of material that is not contained in arXiv:1407.3394. It also does not cover some material that is covered in arXiv:1407.3394.
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 …
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.
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 …
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.
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 …
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 Kapulkin et al. 2012).
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 …
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({\cal C},p)$ defined by a universe $p$ in a locally cartesian closed category $\cal 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 version introduces some changes compared to the previous one to ensure rigorous compatibility with arXiv:1409.7925v3.
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 …
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-Lof 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.
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 …
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.
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 …
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.
This is a major update of the previous version. The methods of the paper are now fully constructive and the style is ready with the emphasis on the possibility of …
This is a major update of the previous version. The methods of the paper are now fully constructive and the style is ready with the emphasis on the possibility of formalization both in type theory and in constructive set theory without the axiom of choice.
This is the third paper in a series started in 1406.7413. In it we construct a C-system $CC({\cal C},p)$ starting from a category $\cal C$ together with a morphism $p:\widetilde{U}\rightarrow U$, a choice of pull-back squares based on $p$ for all morphisms to $U$ and a choice of a final object of $\cal C$. Such a quadruple is called a universe category. We then define universe category functors and construct homomorphisms of C-systems $CC({\cal C},p)$ defined by universe category functors. As a corollary of this construction and its properties we show that the C-systems corresponding to different choices of pull-backs and final objects are constructively isomorphic.
In the second part of the paper we provide for any C-system CC three constructions of pairs $(({\cal C},p),H)$ where $({\cal C},p)$ is a universe category and $H:CC\rightarrow CC({\cal C},p)$ is an isomorphism.
In the third part we define, using the constructions of the previous parts, for any category $C$ with a final object and fiber products a C-system $CC(C)$ and an equivalence $(J^*,J_*):C \rightarrow CC$.
AbstractThis is the second paper in a series started in [13] which aims to provide mathematicaldescriptions of objects and constructions related to the rst few steps of the semantical theoryof …
AbstractThis is the second paper in a series started in [13] which aims to provide mathematicaldescriptions of objects and constructions related to the rst few steps of the semantical theoryof dependent type systems.We construct for any pair ( M;LM ), where M is a monad on sets and LM is a left moduleover M , a C-system (\contextual category) CC ( M;LM ) and describe, using the results of [13]a class of sub-quotients of CC ( M;LM ) in terms of objects directly constructed from M and LM . In the special case of the monads of expressions associated with nominal signatures thisconstruction gives the C-systems of general dependent type theories when they are speci ed bycollections of judgements of the four standard kinds. 1 Introduction The rst few steps in all approaches to the semantics of dependent type theories remain ffitlyunderstood. The constructions which have been worked out in detail in the case of a few particulartype systems by dedicated authors are being extended to the wide variety of type systems underconsideration today by analogy. This is not acceptable in mathematics. Instead we should be ableto obtain the required results for new type systems by
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 …
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 version is essentially identical with the version published in Contemporary Mathematics n.658.
This paper contains a discussion of a library of formalized mathematics for the proof assistant Coq which the author worked on in 2011-13.
This paper contains a discussion of a library of formalized mathematics for the proof assistant Coq which the author worked on in 2011-13.
This is a major update of the previous version. The methods of the paper are now fully constructive and the style is "formalization ready" with the emphasis on the possibility …
This is a major update of the previous version. The methods of the paper are now fully constructive and the style is "formalization ready" with the emphasis on the possibility of formalization both in type theory and in constructive set theory without the axiom of choice. This is the third paper in a series started in 1406.7413. In it we construct a C-system $CC({\cal C},p)$ starting from a category $\cal C$ together with a morphism $p:\widetilde{U}\rightarrow U$, a choice of pull-back squares based on $p$ for all morphisms to $U$ and a choice of a final object of $\cal C$. Such a quadruple is called a universe category. We then define universe category functors and construct homomorphisms of C-systems $CC({\cal C},p)$ defined by universe category functors. As a corollary of this construction and its properties we show that the C-systems corresponding to different choices of pull-backs and final objects are constructively isomorphic. In the second part of the paper we provide for any C-system CC three constructions of pairs $(({\cal C},p),H)$ where $({\cal C},p)$ is a universe category and $H:CC\rightarrow CC({\cal C},p)$ is an isomorphism. In the third part we define, using the constructions of the previous parts, for any category $C$ with a final object and fiber products a C-system $CC(C)$ and an equivalence $(J^*,J_*):C \rightarrow CC$.
In this paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we rst give a new technique …
In this paper, we construct and investigate a model of the Univalent Foundations of Mathematics in the category of simplicial sets. To this end, we rst give a new technique for constructing models of dependent type theory, using universes to obtain coherence. We then construct a (weakly) universal Kan bration, 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 our model. As a corollary, we conclude that Univalent Foundations are at least as consistent as ZFC with two inaccessible cardinals.
This is the text of my talk at CMU on Feb. 4, 2010 were I gave the second public presentation of the Univalence Axiom (called "equivalence axiom" in the text). …
This is the text of my talk at CMU on Feb. 4, 2010 were 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.
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 …
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.
This is the second paper in a series that aims to provide mathematical descriptions of objects and constructions related to the first few steps of the semantical theory of dependent …
This is the second paper in a series 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.
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 …
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 version is essentially identical with the version published in Contemporary Mathematics n.658.
In this paper we give a preliminary formalization of the p-adic numbers, in the context of the second author's univalent foundations program. We also provide the corresponding code verifying the …
In this paper we give a preliminary formalization of the p-adic numbers, in the context of the second author's univalent foundations program. We also provide the corresponding code verifying the construction in the proof assistant Coq. Because work in the univalent setting is ongoing, the structure and organization of the construction of the p-adic numbers we give in this paper is expected to change as Coq libraries are more suitably rearranged, and optimized, by the authors and other researchers in the future. So our construction here should be deemed as a first approximation which is subject to improvements.
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of …
Homotopy type theory is a new branch of mathematics, based on a recently discovered connection between homotopy theory and type theory, which brings new ideas into the very foundation of mathematics. On the one hand, Voevodsky's subtle and beautiful "univalence axiom" implies that isomorphic structures can be identified. On the other hand, "higher inductive types" provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory. Both are impossible to capture directly in classical set-theoretic foundations, but when combined in homotopy type theory, they permit an entirely new kind of "logic of homotopy types". This suggests a new conception of foundations of mathematics, with intrinsic homotopical content, an "invariant" conception of the objects of mathematics -- and convenient machine implementations, which can serve as a practical aid to the working mathematician. This book is intended as a first systematic exposition of the basics of the resulting "Univalent Foundations" program, and a collection of examples of this new style of reasoning -- but without requiring the reader to know or learn any formal logic, or to use any computer proof assistant.
We present an accessible account of Voevodsky's construction of a univalent universe of Kan fibrations.
We present an accessible account of Voevodsky's construction of a univalent universe of Kan fibrations.
The original goal that ultimately led to this volume was the construction of "motivic cohomology theory," whose existence was conjectured by A. Beilinson and S. Lichtenbaum. This is achieved in …
The original goal that ultimately led to this volume was the construction of "motivic cohomology theory," whose existence was conjectured by A. Beilinson and S. Lichtenbaum. This is achieved in the book's fourth paper, using results of the other papers whose additional role is to contribute to our understanding of various properties of algebraic cycles. The material presented provides the foundations for the recent proof of the celebrated "Milnor Conjecture" by Vladimir Voevodsky. The theory of sheaves of relative cycles is developed in the first paper of this volume. The theory of presheaves with transfers and more specifically homotopy invariant presheaves with transfers is the main theme of the second paper. The Friedlander-Lawson moving lemma for families of algebraic cycles appears in the third paper in which a bivariant theory called bivariant cycle cohomology is constructed. The fifth and last paper in the volume gives a proof of the fact that bivariant cycle cohomology groups are canonically isomorphic (in appropriate cases) to Bloch's higher Chow groups, thereby providing a link between the authors' theory and Bloch's original approach to motivic (co-)homology.
Over the past few years it has become apparent that there is a surprising and deep connection between constructive logic and higherdimensional structures in algebraic topology and category theory, in …
Over the past few years it has become apparent that there is a surprising and deep connection between constructive logic and higherdimensional structures in algebraic topology and category theory, in the form of an interpretation of the dependent type theory of Per Martin-Löf into classical homotopy theory. The interpretation results in a bridge between the worlds of constructive and classical mathematics which promises to shed new light on both. This mini-workshop brought together researchers in logic, topology, and cognate fields in order to explore both theoretical and practical ramifications of this discovery.
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 …
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.
Abstract The simplicial extension of any functor from Sets to Sets which commutes with directed colimits respects weak equivalences. In the present paper we construct a framework which allows one …
Abstract The simplicial extension of any functor from Sets to Sets which commutes with directed colimits respects weak equivalences. In the present paper we construct a framework which allows one to extend this result to a wide class of model categories and functors between such categories.
Abstract This paper was written as a part of [8] and is intended primarily to provide the definitions and results concerning motives over simplicial schemes, which are used in the …
Abstract This paper was written as a part of [8] and is intended primarily to provide the definitions and results concerning motives over simplicial schemes, which are used in the proof of the Bloch-Kato conjecture.
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 $$\underline{Hom}({\bold …
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 $$\underline{Hom}({\bold Z}{tr}(X),{\bold Z}{tr}(Y))\rightarrow \underline{Hom}({\bold Z}{tr}(X)\otimes{tr}{\bold G}m,{\bold Z}{tr}(Y)\otimes\_{tr}{\bold G}\_m)$$ is a (weak) ${\bold A}^1$-homotopy equivalence. As a corollary we deduce that the Tate motive is quasi-invertible in the triangulated categories of motives over perfect fields.
In this paper we give a proof of the Bloch-Kato conjecture relating motivic cohomology and etale cohomology. It is a corrected version of the paper with the same title which …
In this paper we give a proof of the Bloch-Kato conjecture relating motivic cohomology and etale cohomology. It is a corrected version of the paper with the same title which posted earlier.
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 …
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 version is essentially identical with the version published in Contemporary Mathematics n.658.
Abstract The simplicial extension of any functor from Sets to Sets which commutes with directed colimits respects weak equivalences. In the present paper we construct a framework which allows one …
Abstract The simplicial extension of any functor from Sets to Sets which commutes with directed colimits respects weak equivalences. In the present paper we construct a framework which allows one to extend this result to a wide class of model categories and functors between such categories.
In this paper we give a direct geometric proof of the fact that tensoring with the Tate motive in the triangulated category of effective motives DM is a full embedding. …
In this paper we give a direct geometric proof of the fact that tensoring with the Tate motive in the triangulated category of effective motives DM is a full embedding. The main part of the proof is given in the context of schemes of finite type over a noetherian base scheme.
Localization of model category structures: Summary of part 1 Local spaces and localization The localization model category for spaces Localization of model categories Existence of left Bousfield localizations Existence of …
Localization of model category structures: Summary of part 1 Local spaces and localization The localization model category for spaces Localization of model categories Existence of left Bousfield localizations Existence of right Bousfield localizations Fiberwise localization Homotopy theory in model categories: Summary of part 2 Model categories Fibrant and cofibrant approximations Simplicial model categories Ordinals, cardinals, and transfinite composition Cofibrantly generated model categories Cellular model categories Proper model categories The classifying space of a small category The Reedy model category structure Cosimplicial and simplicial resolutions Homotopy function complexes Homotopy limits in simplicial model categories Homotopy limits in general model categories Index Bibliography.
We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower …
We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower of iterated identity types over that type. We show that the ω-categories arising in this way are in fact ω-groupoids.
Assume that the category C has a final object * and let X • be a simplicial object in C. For any n 0 we define a n-cube Y = …
Assume that the category C has a final object * and let X • be a simplicial object in C. For any n 0 we define a n-cube Y = cube n (X • ) setting Y i0,...
An analogue of Hilbert's Theorem 90 is proved for the Milnor groups of the fields . Specifically, let be a quadratic extension, and let be the generator of the Galois …
An analogue of Hilbert's Theorem 90 is proved for the Milnor groups of the fields . Specifically, let be a quadratic extension, and let be the generator of the Galois group. Then the sequence is exact. As a corollary one can prove bijectivity of the norm residue homomorphism of degree three: Finally, the 2-primary torsion in is described: if the field contains a primitive th root of unity , then the -torsion subgroup of is . Bibliography: 17 titles.
1. Summary Let 57 * denote the Steenrod algebra corrresponding to an odd prime p. (See ? 2 for definitions.) Our basic results (? 3) is that 5i* is a …
1. Summary Let 57 * denote the Steenrod algebra corrresponding to an odd prime p. (See ? 2 for definitions.) Our basic results (? 3) is that 5i* is a Hopf
The basic purpose of this paper is to prove bijectivity of the norm residue homomorphism for any field of characteristic prime to . In particular, if , then any central …
The basic purpose of this paper is to prove bijectivity of the norm residue homomorphism for any field of characteristic prime to . In particular, if , then any central simple algebra of exponent is similar to a tensor product of cyclic algebras. In the course of the proof we obtain partial degeneracy of the Gersten spectral sequence, and we compute some -cohomology groups of Severi-Brauer groups corresponding to cyclic algebras of prime degree. The fundamental theorem also gives us several corollaries.
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 …
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 Z/2-coefficients. This paper is a new version of the previously distributed preprint "The Milnor Conjecture".
We give a new proof of the theorem of Suslin-Voevodsky which shows that the Bloch-Kato conjecture implies a portion of the BeilinsonLichtenbaum conjectures. Our proof does not rely on resolution …
We give a new proof of the theorem of Suslin-Voevodsky which shows that the Bloch-Kato conjecture implies a portion of the BeilinsonLichtenbaum conjectures. Our proof does not rely on resolution of singularities, and thereby extends the Suslin-Voevodsky theorem to positive characteristic.
This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing …
This paper presents a novel connection between homotopical algebra and mathematical logic. It is shown that a form of intensional type theory is valid in any Quillen model category, generalizing the Hofmann-Streicher groupoid model of Martin-Loef type theory.
AbstractThis is the second paper in a series started in [13] which aims to provide mathematicaldescriptions of objects and constructions related to the rst few steps of the semantical theoryof …
AbstractThis is the second paper in a series started in [13] which aims to provide mathematicaldescriptions of objects and constructions related to the rst few steps of the semantical theoryof dependent type systems.We construct for any pair ( M;LM ), where M is a monad on sets and LM is a left moduleover M , a C-system (\contextual category) CC ( M;LM ) and describe, using the results of [13]a class of sub-quotients of CC ( M;LM ) in terms of objects directly constructed from M and LM . In the special case of the monads of expressions associated with nominal signatures thisconstruction gives the C-systems of general dependent type theories when they are speci ed bycollections of judgements of the four standard kinds. 1 Introduction The rst few steps in all approaches to the semantics of dependent type theories remain ffitlyunderstood. The constructions which have been worked out in detail in the case of a few particulartype systems by dedicated authors are being extended to the wide variety of type systems underconsideration today by analogy. This is not acceptable in mathematics. Instead we should be ableto obtain the required results for new type systems by
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 …
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.
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 …
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 Kapulkin et al. 2012).
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 …
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.
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 …
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 A^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 term-wise ind-solid simplicial sheaves.
Since the beginning of the modern era of algebraic topology, simplicial methods have been used systematically and effectively for both computation and basic theory. With the development of Quillen's c
Since the beginning of the modern era of algebraic topology, simplicial methods have been used systematically and effectively for both computation and basic theory. With the development of Quillen's c