  In this paper we present our current development on a new formalization of
nominal sets in Agda. Our first motivation in having another formalization was
to understand better nominal sets and to have a playground for testing type
systems based on nominal logic. Not surprisingly, we have independently built
up the same hierarchy of types leading to nominal sets. We diverge from other
formalizations in how to conceive finite permutations: in our formalization a
finite permutation is a permutation (i.e. a bijection) whose domain is finite.
Finite permutations have different representations, for instance as
compositions of transpositions (the predominant in other formalizations) or
compositions of disjoint cycles. We prove that these representations are
equivalent and use them to normalize (up to composition order of independent
transpositions) compositions of transpositions.
