An Equivalent Presentation of the Bezem-Coquand-Huber Category of Cubical Sets
Staton has shown that there is an equivalence between the category of
presheaves on (the opposite of) finite sets and partial bijections and
the category of nominal restriction sets: see [2, Exercise 9.7]. The
aim here is to see that this extends to an equivalence between the
category of cubical sets introduced in [1] and a category of nominal
sets equipped with a "01-substitution" operation. It seems to me that
presenting the topos in question equivalently as 01-substitution sets
rather than cubical sets will make it easier (and more elegant) to
carry out the constructions and calculations needed to build the
intended univalent model of intentional constructive type theory.
Last modified: Thu Jan 30 11:59:32 GMT 2014