Simplicial sets inside cubical sets

TL;DR

This paper demonstrates how the topos of simplicial sets can be embedded within the topos of cubical sets, constructing a fibrant univalent universe for sheaves and exploring their relation to homotopy theory models.

Contribution

It constructs a fibrant univalent universe within cubical sets for sheaves, enabling the embedding of simplicial sets into univalent type theory models.

Findings

Constructed a fibrant univalent universe in cubical sets.

Enabled the interpretation of simplicial sets as a submodel for univalent type theory.

Reformulated the relation between model structures in cubical sets and homotopy theory.

Abstract

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 sheaves. This makes it possible to consider $\mathbf{sSet}$ as a submodel of $\mathbf{cSet}$ for univalent Martin-L\"of type theory. Furthermore, we address the question whether the type-theoretic Cisinski model structure considered on $\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.