I just saw that Andy Pitts has a new draft out, An Equivalent Presentation of the Bezem-Coquand-Huber Category of Cubical Sets, with the following abstract:
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.
Nominal methods have been an active area of research in PL theory for a while now, and have achieved a rather considerable level of sophistication. I have occasionally joked that it seems like we had to aim an awful lot of technical machinery at the problem of alpha-equivalence -- so what happens when we realize that there are other equivalence relations in mathematics?
But with this note, it looks like the last laugh is on me!
Pitts shows that you can use nominal techniques to give a simpler presentation of the cubical sets model of univalent type theory. Since HoTT gives us a clean constructive account of quotient types and higher inductive types, all the technical machinery invented to handle alpha-equivalence scales smoothly up to handle any equivalence relation you like.
