  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.
