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

Research output: Unpublished contribution to conferenceUnpublished abstract

25 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.
Original languageEnglish
Number of pages3
Publication statusPublished - 23 Aug 2020
EventWorkshop on Type-Driven Development - Online, Jersey City, United States
Duration: 23 Aug 202023 Aug 2020


WorkshopWorkshop on Type-Driven Development
Abbreviated titleTyDe
CountryUnited States
CityJersey City
Internet address

Cite this