Sciweavers

Share
ENTCS
2008

Towards Formalizing Categorical Models of Type Theory in Type Theory

9 years 1 days ago
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.
Alexandre Buisse, Peter Dybjer
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where ENTCS
Authors Alexandre Buisse, Peter Dybjer
Comments (0)
books