单纯集和三次集的拓扑中的层次

Cubical models of higher categories without connections

We prove that each of the model structures for ($n$-trivial, saturated) comical sets on the category of marked cubical sets having only faces and degeneracies (without connections) is Quillen equivalent to the corresponding model structure for ($n$-trivial, saturated) complicial sets on the category of marked simplicial sets, as well as to the corresponding comical model structures on cubical sets with connections. As a consequence, we show that the cubical Joyal model structure on cubical sets without connections is equivalent to its analogues on cubical sets with connections and to the Joyal…

Simplicial sets inside cubical sets

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…

Cubical rigidification, the cobar construction, and the based loop space

We prove the following generalization of a classical result of Adams: for any pointed and connected topological space $(X,b)$, that is not necessarily simply connected, the cobar construction of the differential graded (dg) coalgebra of normalized singular chains in $X$ with vertices at $b$ is weakly equivalent as a differential graded associative algebra (dga) to the singular chains on the Moore based loop space of $X$ at $b$. We deduce this statement from several more general categorical results of independent interest. We construct a functor $\mathfrak{C}_{\square_c}$ from simplicial sets t…

Cubical models of $(\infty, 1)$-categories

We construct a model structure on the category of cubical sets with connections whose cofibrations are the monomorphisms and whose fibrant objects are defined by the right lifting property with respect to inner open boxes, the cubical analogue of inner horns. We show that this model structure is Quillen equivalent to the Joyal model structure on simplicial sets via the triangulation functor. As an application, we show that cubical quasicategories admit a convenient notion of a mapping space, which we use to characterize the weak equivalences between fibrant objects in our model structure as DK…

Cubical sets and the topological topos

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…

Eilenberg-Steenrod homology and cohomology theories for Čech's closure spaces

We generalize some of the fundamental results of algebraic topology from topological spaces to Čech's closure spaces, also known as pretopological spaces. Using simplicial sets and cubical sets with connections, we define three distinct singular (relative) simplicial and six distinct singular (relative) cubical (co)homology groups of closure spaces. Using acyclic models we show that the three simplicial groups have isomorphic cubical analogues among the six cubical groups. Thus, we obtain a total of six distinct singular (co)homology groups of closure spaces. Each of these is shown to have a c…

立方集和图的同伦n-型

Homotopy $n$-types of cubical sets and graphs

本文提出了一种基于右传递的模型结构构造方法，用于在立方集和图的范畴中定义同伦n-型的纤维范畴结构。

另一种立方类型理论，但通过语义方法

Yet another cubical type theory, but via a semantic approach

本文提出了一种新的立方类型理论，并通过宇宙范畴框架研究其语义学，展示了其在多种数学结构中的解释能力。

Induced model structures for higher categories

We give a new criterion guaranteeing existence of model structures left-induced along a functor admitting both adjoints. This works under the hypothesis that the functor induces idempotent adjunctions at the homotopy category level. As an application, we construct new model structures on cubical sets, prederivators, marked simplicial sets and simplicial spaces modeling $\infty$-categories and $\infty$-groupoids.

Idempotent completion of cubes in posets

This note concerns the category $\Box$ of cartesian cubes with connections, equivalently the full subcategory of posets on objects $[1]^n$ with $n \geq 0$. We show that the idempotent completion of $\Box$ consists of finite complete posets. It follows that cubical sets, ie presheaves over $\Box$, are equivalent to presheaves over finite complete posets. This yields an alternative exposition of a result by Kapulkin and Voevodsky that simplicial sets form a subtopos of cubical sets.

通过项链构造的充实范畴神经

Nerves of enriched categories via necklaces

本文提出项链神经函子统一了同伦相干神经、微分分次神经和立方神经，证明其可提升为templicial对象，并给出左伴随的显式描述条件，从而得到dg-神经与立方神经左伴随的新简洁表达式。

The Equivalence Extension Property and Model Structures

We give an elementary construction of a certain class of model structures. In particular, we rederive the Kan model structure on simplicial sets without the use of topological spaces, minimal complexes, or any concrete model of fibrant replacement such as Kan's Ex^infinity functor. Our argument makes crucial use of the glueing construction developed by Cohen et al. in the specific setting of certain cubical sets.