Shallowly Embedding Type Theories as Presheaf Models in Agda (Extended Abstract)
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|
Sun 23 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
|10:00 - 10:30|
Víctor López JuanChalmers University of Technology, Nils Anders DanielssonUniversity of Gothenburg, Chalmers University of TechnologyMedia Attached
|10:30 - 11:00|
|11:00 - 11:30|