This repository contains formalisations accompanying the following papers:
Type Theory in Type Theory using Quotient Inductive Types (POPL 2016)
Normalisation by Evaluation for Dependent Types (FSCD 2016)
Normalisation by Evaluation for Type Theory, in Type Theory (submitted to LMCS)
by Thorsten Altenkirch and Ambrus Kaposi,
and the PhD thesis of Ambrus Kaposi titled
- Type theory in a type theory with quotient inductive types
See Readme.agda for more information.