We present work in progress on a shallow embedding of extensions of Martin-Löf Type Theory (MLTT) in Agda as presheaf models. In this way, a user wanting to explore some extension of MLTT can do so by instantiating our framework with a suitable base category, implementing the desired operations and axioms and then he/she can manipulate types and terms of the system in a similar way as in MLTT.
|Number of pages||3|
|Publication status||Published - 23 Aug 2020|
|Event||Workshop on Type-Driven Development - Online, Jersey City, United States|
Duration: 23 Aug 2020 → 23 Aug 2020
|Workshop||Workshop on Type-Driven Development|
|Period||23/08/20 → 23/08/20|