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:

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