A Logical Relation for Dependent Type Theory Formalized in Agda

Abstract: When writing proofs, it is desirable to show that one’s proof is correct. With formalising a proof in dependent type theory, it is implied that the proof is correct as long as the type theory is correct.

This thesis covers the formalisation of a fragment of Martin-Löf type theory with one universe, for which its grammar and judgements are formalised. A logical relation is then defined as well as validity judgements and proven valid with respect to the type system. This is then used to prove canonicity and injectivity of the II -type.