A Logical Relation for Martin-Löf Type Theory in Agda
This is a project to formalize a proof of the decidability of conversion of a dependently typed language in Agda. The source code for the paper can be browsed in HTML here. Since then, the project has been extended with an empty type, unit type and dependent sums.
This project is written in Agda. It has been tested to be working with Agda version 2.6.1.