English

Simplicial sets inside cubical sets

Category Theory 2021-03-15 v2

Abstract

As observed recently by various people the topos sSet\mathbf{sSet} of simplicial sets appears as essential subtopos of a topos cSet\mathbf{cSet} of cubical sets, namely presheaves over the category FL\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 cSet\mathbf{cSet} a fibrant univalent universe for those types that are sheaves. This makes it possible to consider sSet\mathbf{sSet} as a submodel of cSet\mathbf{cSet} for univalent Martin-L\"of type theory. Furthermore, we address the question whether the type-theoretic Cisinski model structure considered on cSet\mathbf{cSet} coincides with the test model structure, the latter of which models the homotopy theory of spaces. We do not provide an answer to this open problem, but instead give a reformulation in terms of the adjoint functors at hand.

Keywords

Cite

@article{arxiv.1911.09594,
  title  = {Simplicial sets inside cubical sets},
  author = {Thomas Streicher and Jonathan Weinberger},
  journal= {arXiv preprint arXiv:1911.09594},
  year   = {2021}
}

Comments

11 pages; some expansion esp. in Sections 4 and 5; accepted for publication in Theory and Applications of Categories

R2 v1 2026-06-23T12:23:36.820Z