There are two natural ways of excluding an atom a in nominal
techniques: we can either
consider the sets X such that a is fresh for X, or we can consider the
sets X such that a is
fresh for every x ∈ X.
The statements of 'being fresh for all the elements of that set' and
'being fresh for a set'
are not the same: it is not the case that ∀x ∈ X.a#x if
and only if a#X.
Both notions encode natural notions of 'fresh a'. In this paper, it is
proved that these
notions lead naturally to two categories that are isomorphic, so that
in a suitable generalised
sense they are the same.
The result is mathematically attractive and has an interesting
reading: it is equivalent
to add a fresh atom to the underlying universe, and to add a symbol to
the meta-language
referencing a fresh atom. Or to put it slightly differently: we prove
the intuitively appealing
but non-obvious fact that a fresh atom in the object-level is
categorically isomorphic to a
fresh atom in the meta-level.
| 
