  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.
