Article
Nominal sets in Agda
Fecha
2022Autor
Pagano, Miguel
Solsona, Jose E.
Institución
Resumen
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.