# Nominal Sets in Lean 4

WIP formalization of nominal sets in Lean 4.
The formalization is mostly based on:
- Pitts, A. M. Nominal Sets: Names and Symmetry in Computer Science. Cambridge Tracts in Theoretical Computer Science 57. Cambridge University Press, 2013.
- Wißmann, Thorsten. Nominal Sets. Skript zur Vorlesung. FAU Erlangen-Nürnberg, October 11, 2024. https://www8.cs.fau.de/ext/teaching/sose2024/nominal-sets/nominal-sets-wissmann-skript.pdf.

The library is structured as follows:
- `Nominal.Permutations`: 
  Definition of the subgroup `FPerm` of finitely supported permutations and of `PermSet`s (i.e., sets on which `FPerm` operates).
- `Nominal.Support`:
  Definition of support, nominal sets, the least finite support, and some helpers.
- `Nominal.Equivariance`:
  Definition of equivariant functions, sets, and relations and some helper lemmas about them.
- `Nominal.Category`:
  Definition of the `Nom` category.
- `Nominal.Instances.Basic`:
  Some basic instances of nominal sets: discrete nominal sets, the set of atoms, products, coproducts, finitary functions, quotient types, and subtypes.
- `Nominal.Instances.Abstraction`:
  Definition of name abstractions and alpha-equivalence, followed by the name abstraction functor.
- `Nominal.Instances.Finsupp`:
  Definition of subsets of `PermSet`s with finite support, especially finitely supported sets and functions.
- `Nominal.LambdaCalculus.Preterms`:
  Lambda terms as an example of nominal sets, showing that `supp` corresponds to the variables in a term.
- `Nominal.LambdaCalculus.Terms`:
  Lambda terms modulo alpha-equivalence as an example, showing that `supp` corresponds to the free variables in a term.