Simplicial sets inside cubical sets
Abstract
As observed recently by various people the topos of simplicial sets appears as essential subtopos of a topos of cubical sets, namely presheaves over the category 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 a fibrant univalent universe for those types that are sheaves. This makes it possible to consider as a submodel of for univalent Martin-L\"of type theory. Furthermore, we address the question whether the type-theoretic Cisinski model structure considered on 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.
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