A fundamental component of homotopy type theory, a synthetic theory of $\infty$-groupoids, is Voevodsky's univalence axiom. Univalence characterizes the identity types in the universal fibration, a classifier for small type families: identity types in the universe are equivalent to types of equivalences. The directed univalence axiom plays a similar foundational role in simplicial type theory, a synthetic theory of $\infty$-categories. In its original form, which does not include universes or directed univalence, the simplicial type theory has semantics in categories of simplicial objects in an $\infty$-topos, with synthetic $\infty$-categories corresponding to internal $\infty$-categories. We verify that directed univalence holds in this semantic setting, constructing an equivalence between hom types in the universal left fibration and function types. In fact, we verify a higher version of this result, constructing an equivalence between homotopy coherent composites in the universal left fibration and composable sequences of functions between types. Using the technique of weighted limits, we reduce this theorem for simplicial objects in an arbitrary $\infty$-topos to calculations "on the left" with simplicial sets.
A modest Kan complex is a modest simplicial set which has a right lifting property with respect to horn inclusions $Λ_k[n] \to Δ[n]$. This paper develops the categorical logical that is required to show that there is a univalent universe of modest Kan complexes among simplicial assemblies.
We construct a new model category presenting the homotopy theory of presheaves on "inverse EI $(\infty,1)$-categories", which contains universe objects that satisfy Voevodsky's univalence axiom. In addition to diagrams on ordinary inverse categories, as considered in previous work of the author, this includes a new model for equivariant algebraic topology with a compact Lie group of equivariance. Thus, it offers the potential for applications of homotopy type theory to equivariant homotopy theory.
Univalence was first defined in the setting of homotopy type theory by Voevodsky, who also (along with Kapulkin and Lumsdaine) adapted it to a model categorical setting, which was subsequently generalized to locally Cartesian closed presentable $\infty$-categories by Gepner and Kock. These definitions were used to characterize various $\infty$-categories as models of type theories. We give a definition for univalent morphisms in finitely complete $\infty$-categories that generalizes the aforementioned definitions and completely focuses on the $\infty$-categorical aspects, characterizing it via…
After developing the basic theory of locally cartesian localizations of presentable locally cartesian closed infinity-categories, we establish the representability of equivalences and show that univalent families, in the sense of Voevodsky, form a poset isomorphic to the poset of bounded local classes, in the sense of Lurie. It follows that every infinity-topos has a hierarchy of "universal" univalent families, indexed by regular cardinals, and that n-topoi have univalent families classifying (n-2)-truncated maps. We show that univalent families are preserved (and detected) by right adjoints t…
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 maps between them. The latter is a variant of the cubical model of type theory due to Cohen et al. for the purpose of providing a model for a variant of type theory which validates Voevodsky's Univalence Axiom and has computational meaning. Our contribution consists in constructing in $\mathbf{cSet}$ a fibrant univalent universe for those types that are shea…
In this paper we consider simplicial families, that is, simplicial objects indexed by a simplicial set. We develop a method to construct family hypercover refinements of a cover family based on the notion of \emph{n-spans} that we introduce here. In [The fundamental progroupoid of a general topos, Journal of Pure and Applied Algebra 212 (2008)] we had introduced the notion of \emph{covering projection} in a topos. They are locally constant objects satisfying an additional condition which is valid in all locally constant objects when the topos is locally connected, and developed the theory of t…
Coquand's cubical set model for homotopy type theory provides the basis for a computational interpretation of the univalence axiom and some higher inductive types, as implemented in the cubical proof assistant. This paper contributes to the understanding of this model. We make three contributions: 1. Johnstone's topological topos was created to present the geometric realization of simplicial sets as a geometric morphism between toposes. Johnstone shows that simplicial sets classify strict linear orders with disjoint endpoints and that (classically) the unit interval is such an order. Here we s…
We observe that the category of topological space, uniform spaces, and simplicial sets are all, in a natural way, full subcategories of the same larger category, namely the simplicial category of filters; this is, moreover, implicit in the definitions of a topological and uniform space. We use these embeddings to rewrite the notions of completeness, precompactness, compactness, Cauchy sequence, and equicontinuity in the language of category theory, which we hope might be of use in formalisation of mathematics and tame topology. We formulate some arising open questions.
This paper aims to help the development of new models of homotopy type theory, in particular with models that are based on realizability toposes. For this purpose it develops the foundations of an internal simplicial homotopy that does not rely on classical principles that are not valid in realizability toposes and related categories.
A definable type of a first-order theory is the same as a section (retraction) of the simplicial path space (decalage) of its space of types viewed as a simplicial topological space; as is well-known, in the category of simplicial sets such sections correspond to homotopies contracting each connected component. Without the simplicial language this is stated in Exercise 8.3.3 in the model theory textbook [Tent-Ziegler], which defines a bijection between the set of all $1$-types definable over a parameter set $B$ and the set of all "coherent" families of continuous sections $π_n:S^T_n(B)\to S^T_…
