As observed recently by various people the topos sSet of simplicial sets appears as an essential subtopos of a topos cSet of cubical sets, namely presheaves over the category 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 a fibrant univalent universe for those types that are sheaves. This makes it possible to consider sSet as a submodel of cSet for univalent Martin-Löf type theory.
Furthermore, we address the question whether the type-theoretic Cisinski model structure considered on 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: cubical sets, simplicial sets, universes, univalence axiom
2020 MSC: 03B38, 03G30, 18F20, 18N45
Theory and Applications of Categories, Vol. 37, 2021, No. 10, pp 276-286.
Published 2021-03-15.
TAC Home