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.
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…
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…
在本文中，我们考虑单纯的家庭，也就是说，单纯对象索引的单纯集。我们开发了一种方法来构建家庭超覆盖加细的覆盖家庭的基础上的概念，我们在这里介绍的\emph{n-spans}。在[The fundamental progroupoid of a general topos，Journal of Pure and Applied Algebra 212（2008）]中，我们在topos中引入了\emph{covering projection}的概念。它们是局部常数对象，满足一个附加条件，当拓扑是局部连通的时，该条件在所有局部常数对象中都是有效的，并发展了一般拓扑的基本广群理论。在这里，我们表明，覆盖投影可以得到从一个家庭的集合上的单纯集的下降数据构造的对象。我们构造了一个广群$\nn{G}_\cc{H}$，使得被$\cc{H}$平凡化的覆盖投影范畴$\cc{G}_\cc{H}$是它的分类拓扑.这确定了一个原群$\{\cc{G} \cc{H}\}_\cc{H}$和一个progroupoid $\{\nn{G}_\cc{H}\}_\cc{H}$，适合于由超覆盖的过滤偏序集索引。然后，我们表明，这progroupoid分类torsors。这种构造在局部连通拓扑的情况下也是新颖的，表明局部连通拓扑中的局部常数对象是通过从集合族上的下降数据下降而构造的。区分局部连通topoi的显著特征是，pro…
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.
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_…
