The code in this repository is a formalisation of parts of the work in [1]. More precisely, we formalised the raw syntax and the reduction relation, which were given in that paper.
In the future, I would like to have at least the typing rules and the proof of subject reduction formalised.
Requires Agda version 2.6.0.1 and the master branch of the standard library (will be v0.18).
[1] H. Basold and H. Geuvers, ‘Type Theory based on Dependent Inductive and Coinductive Types’, in LICS’16, 2016.