Related papers: Univalence in Simplicial Sets
We present Voevodsky's construction of a model of univalent type theory in the category of simplicial sets. To this end, we first give a general technique for constructing categorical models of dependent type theory, using universes to…
We review the concept of a univalent fibration and show by elementary means that every Kan fibration in simplicial sets can be embedded in a univalent Kan fibration.
We provide a partial solution to the problem of defining a constructive version of Voevodsky's simplicial model of univalent foundations. For this, we prove constructive counterparts of the necessary results of simplicial homotopy theory,…
We construct a univalent universe in the sense of Voevodsky in some suitable model categories for homotopy types (obtained from Grothendieck's theory of test categories). In practice, this means for instance that, appart from the homotopy…
We introduce the notion of an effective Kan fibration, a new mathematical structure that can be used to study simplicial homotopy theory. Our main motivation is to make simplicial homotopy theory suitable for homotopy type theory. Effective…
This PhD thesis deals with some new models of intensional type theory and the Univalence Axiom introduced by Vladimir Voevodsky. Our work takes place in the framework of the definitions of type-theoretic fibration categories (the notion of…
A modest Kan complex is a modest simplicial set which has a right lifting property with respect to horn inclusions $\Lambda_k[n] \to \Delta[n]$. This paper develops the categorical logical that is required to show that there is a univalent…
As observed recently by various people the topos $\mathbf{sSet}$ of simplicial sets appears as essential subtopos of a topos $\mathbf{cSet}$ of cubical sets, namely presheaves over the category $\mathbf{FL}$ of finite lattices and monotone…
We offer an introduction for mathematicians to the univalent foundations of Vladimir Voevodsky, aiming to explain how he chose to encode mathematics in type theory and how the encoding reveals a potentially viable foundation for all of…
We prove that any surjective homomorphism of simplicial Maltsev algebras is a Kan fibration.
This paper investigates Voevodsky's univalence axiom in intensional Martin-L\"of type theory. In particular, it looks at how univalence can be derived from simpler axioms. We first present some existing work, collected together from various…
We develop further the theory of weak factorization systems and algebraic weak factorization systems. In particular, we give a method for constructing (algebraic) weak factorization systems whose right maps can be thought of as (uniform)…
The paper is devoted to an approach to the bounded cohomology theory based on the theories of simplicial sets and Postnikov systems. In particular, the main results of the bounded cohomology theory of topological spaces are extended to…
We describe certain class of simplicial sets introduced by Dmitry Skvortsov and Valentin Shehtman; we call such simplicial sets Skvortsov-Shehtman complexes. An example of a Skvortsov-Shehtman complex that is not a Kan complexes is given.
In this short note we give a glimpse of homotopy type theory, a new field of mathematics at the intersection of algebraic topology and mathematical logic, and we explain Vladimir Voevodsky's univalent interpretation of it. This…
In this article the author endows the functor category [B(C2),Gpd] with the structure of a type-theoretic fibration category with a universe using the projective fibrations. It offers a new model of Martin-L\"of type theory with dependent…
It is obtained a natural generalisation of Uspenskij's selection characterisation of paracompact $C$-spaces. The method developed to achieve this result is also applied to give a simplified proof of a similar characterisation of paracompact…
There are infinitely many variants of the notion of Kan fibration that, together with suitable choices of cofibrations and the usual notion of weak equivalence of simplicial sets, satisfy Quillen's axioms for a homotopy model category. The…
In this note we show that Voevodsky's univalence axiom holds in the model of type theory based on symmetric cubical sets. We will also discuss Swan's construction of the identity type in this variation of cubical sets. This proves that we…
On the category of bisimplicial sets there are different Quillen closed model structures associated to various definitions of fibrations. In one of them, which is due to Bousfield and Kan and that consists of seeing a bisimplicial set as a…