Write a Blog >>
ICFP 2020
Sun 23 - Sat 29 August 2020

We present work in progress on a shallow embedding of extensions of Martin-Löf Type Theory in Agda as presheaf models. More concretely, the terms, types, … of an object theory are represented in Agda using the presheaf construction and a user can manipulate them in the style of a category with families, with variables in de Bruijn form. Extra operations or axioms can be implemented by instantiating the framework with a suitable base category.

Extended Abstract (TyDeAbstract.pdf)343KiB