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.