An Agda formalisation of χ

An Agda formalisation of one variant of χ, along with a number of properties:

• Code listing (with hyperlinked identifiers).

• The code can be obtained by running the following commands (in an empty directory):

  git clone http://www.cse.chalmers.se/~nad/repos/equality/
  git clone http://www.cse.chalmers.se/~nad/repos/chi/

  At the time of writing the code is not accepted by the most recent version of Agda (2.6.0.1), a sufficiently recent development version is required.