Cubical sets as a classifying topos

We will provide a description of the cubical model based on the
internal logic of the topos of cubical sets. To be precise, we will
show what this topos classifies and how this helps us to simplify the
presentation of the model. Specifically, this will allow us to
describe the geometrical realization as a geometric morphism from
Johnstone’s topological topos.

This work is the basis for a semantics of an extension of cubical type
theory with guarded dependent types. The latter part is joint work
within the logic and semantics group in Aarhus.