Towards Formalizing Categorical Models of Type Theory in Type Theory

This note is about work in progress on the topic of “internal type theory” where we investigate the internal formalization of the categorical metatheory of constructive type theory in (an extension of) itself. The basic notion is that of a category with families, a categorical notion of model of dependent type theory. We discuss how to formalize the notion of category with families inside type theory and how to build initial categories with families. Initial categories with families will be term models which play the role of canonical syntax for dependent type theory. We also discuss the formalization of the result that categories with finite limits give rise to categories with families. This yields a type-theoretic perspective on Curien's work on “substitution up to isomorphism”. Our formalization is being carried out in the proof assistant Agda 2 developed at Chalmers.