500 *}

   500 *}

   501 

   501 

   502 section {* Equivariance *}

   502 section {* Equivariance *}

   503 

   503 

   504 text {*

   504 text {*

   505   Two important notions in the nominal logic work are what Pitts calls

   507   Two important notions in the nominal logic work are what Pitts calls

   506   \emph{equivariance} and the \emph{equivariance principle}.  These

   508   \emph{equivariance} and the \emph{equivariance principle}.  These

   507   notions allows us to characterise how permutations act upon compound

   509   notions allows us to characterise how permutations act upon compound

   508   statements in HOL by analysing how these statements are constructed.

   510   statements in HOL by analysing how these statements are constructed.

   509   The notion of equivariance means that an object is invariant under

   511   The notion of equivariance means that an object is invariant under