Shallowly Embedding Type Theories as Presheaf Models in Agda: Extended Abstract

Joris Ceulemans, Dominique Devriese

Onderzoeksoutput: Unpublished abstract

101 Downloads (Pure)


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.
Originele taal-2English
Aantal pagina's3
StatusPublished - 23 aug 2020
EvenementWorkshop on Type-Driven Development - Online, Jersey City, United States
Duur: 23 aug 202023 aug 2020


WorkshopWorkshop on Type-Driven Development
Verkorte titelTyDe
Land/RegioUnited States
StadJersey City
Internet adres

Citeer dit