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/