add readmeHEADmain

1 files changed, 26 insertions, 0 deletions

diff --git a/readme.md b/readme.md
new file mode 100644
index 0000000..00f3c89
--- /dev/null
+++ b/readme.md
@@ -0,0 +1,26 @@
+# 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.
\ No newline at end of file