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

Research output: Unpublished contribution to conferenceUnpublished abstract

11 Downloads (Pure)

Abstract

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
https://icfp20.sigplan.org/home/tyde-2020

Workshop

WorkshopWorkshop on Type-Driven Development
Abbreviated titleTyDe
CountryUnited States
CityJersey City
Period23/08/2023/08/20
Internet address

Cite this