Nominal techniques are based on the idea of sets with a finitely-supported
In this paper we consider the idea of sets with a finitely-supported
atoms-renaming action (renamings can identify atoms; permutations cannot).
We show that these exhibit many of the useful qualities found in
traditional nominal techniques; an elementary sets-based presentation, inductive datatypes of syntax up to binding, cartesian closure, and being
a topos. Unlike in nominal techniques, the notion of names-abstraction
coincides with functional abstraction.