On Initial Categories with Families Formalization of unityped and simply typed CwFs in Agda

Abstract

This thesis explores a categorical model of type theory, namely, categories with families who provide a model for a basic framework of dependent type theory. The notion of a category with families is formalized as a generalized algebraic theory with extra structure with the purpose of modelling different lambda calculi. The work revolves around implementing in the Agda proof assistant categories with families at three levels: (i) untyped, (ii) simply typed, and (iii) dependently typed calculi. The formalization primarily consists of constructing initial objects in the category of categories with families and isomorphisms between them. The work investigates each notion from its core and proceeds by adding extra structure. Complete formalizations of untyped and simply typed categories with families are presented along with an incomplete picture for dependent types.