2019/11/21 by Thomas Streicher, Streicher, Thomas, Jonathan Weinberger +1
Mathematics · #03B38 #03G30 #18F20 #18N45 #Advanced Topology and Set Theory #Category Theory (math.CT) #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology
paper · pdf · doi:10.48550/arxiv.1911.09594
openalex publication_date 2019/11/21 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
As observed recently by various people the topos sSet of simplicial sets appears as 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.