module README where

{- 
This is a constructive development of the theory of nominal sets in Agda v2.4.2.3,
done as part of the MPhil ACS project `Constructive  Representation of Nominal 
Sets in Agda' by Pritam Choudhury under the supervision of Prof. Andrew M Pitts.
This file gives an outline of the different modules developed as part of this project.
-}

{-
The basic definitions including those given in Definition 1.1 and Definition 1.2 of 
Chapter 1 can be found in Basics.agda. This file acts as a library for all the basic
definitions used by other files.
-}

open import Basics

{-
The basic definitions and properties of Atoms including those in Definitions 1.4-1.6, 
Lemma 1.7, Definition 1.8, Lemma 1.9 and Lemma 1.10 can be found in Atoms.agda.
-}

open import Atoms

{- 
The basic definitions and properties pertaining to permutations including those in
Definition 2.1, Definition 2.2, Definition 2.4, Lemma 2.5, Lemma 2.6, 
Definition 2.8, Lemma 2.11, Lemma 2.12, Definition 2.15, Lemma 2.16, Lemma
2.17, Lemma 2.18 can be found in Perms.agda.
-}

open import Perms

{-
The other important properties of permutations including those in Lemma 2.3,
Definition 2.22, Lemma 2.23, Lemma 2.24, Corollary 2.25, Corollary 2.26,
Corollary 2.27, Corollary 2.28 can be found in PermProp.agda.
-}

open import PermProp

{-
The definitions of group and group action with some examples (Definition 2.9,
Theorem 2.10, Definition 2.13, Section 2.8) can be found in Group.agda.
-}

open import Group

{-
The definition of PermSet (Definition 2.19), equivariant functions on PermSets
(Definition 2.20), example of an equivariant function (Lemma 2.21) can be found 
in PermSet.agda.
-}

open import PermSet

{- 
The basic definitions of category theory (given in Chapter 3) can be found in
CatDef.agda.
-}

open import CatDef

{-
The definition of nominal set (Definition 3.1) and the category theoretic properties
of nominal sets and equivariant functions (Section 3.4-3.8) can be found in Nom.agda.
-}

open import Nom

{-
Some examples of nominal sets, as given in Section 3.2, can be found in NomSet.agda.
-}

open import NomSet

{-
The category theoretic properties of nominal sets and finitely supported functions 
(Section 3.4-3.8) can be found in Nomfs.agda.
-}

open import Nomfs

{-
The relation between PermSets and NomSets, as presented in Sections 3.9 and 3.10,
can be found in CoSub.agda
-}

open import CoSub

{-
The properties of the freshness relation, as developed in Chapter 4, can be found in
FreshNom.agda
-}

open import FreshNom

{-
The definition and properties of name abstraction including those in Definition 5.1,
Lemmas 5.2-5.9 can be found in NameAbst.agda
-}

open import NameAbst

{-
Some of the properties of name abstraction functor (Lemmas 5.10-5.12) can be found
in AbsProp.agda
-}

open import AbsProp

{-
Theorem 5.13 can be found in Adj.agda
-}

open import Adj

{-
The theorems related to Freshness Condition for Binders (Section 5.5) can 
be found in FreshCon.agda
-}

open import FreshCon  

--This concludes our development of nominal sets in Agda.

-------------------------------------------------------------------------------------------