On generalized algebraic theories and categories with families. (18th October 2021)

• Record Type: Journal Article
• Authors: Bezem, Marc; Coquand, Thierry; Dybjer, Peter; Escardó, Martín
• Is Part Of: Mathematical structures in computer science. Volume 31:Number 9(2021)
• Page Start: 1006
• Page End: 1023
• Publication Date: 2021-10-18
• Subjects: Dependent type theory -- generalized algebraic theory -- category with families -- initial model -- internal category -- Martin-Löf type theory; Computer science -- Mathematics -- Periodicals; 004.015105
• DOI: 10.1017/S0960129521000268
• Languages: English
• ISSNs: 0960-1295

Abstract

Abstract: We give a syntax independent formulation of finitely presented generalized algebraic theories as initial objects in categories of categories with families (cwfs) with extra structure. To this end, we simultaneously define the notion of a presentation Σ of a generalized algebraic theory and the associated category CwF Σ of small cwfs with a Σ-structure and cwf-morphisms that preserve Σ-structure on the nose. Our definition refers to the purely semantic notion of uniform family of contexts, types, and terms in CwF Σ . Furthermore, we show how to syntactically construct an initial cwf with a Σ-structure. This result can be viewed as a generalization of Birkhoff's completeness theorem for equational logic. It is obtained by extending Castellan, Clairambault, and Dybjer's construction of an initial cwf. We provide examples of generalized algebraic theories for monoids, categories, categories with families, and categories with families with extra structure for some type formers of Martin-Löf type theory. The models of these are internal monoids, internal categories, and internal categories with families (with extra structure) in a small category with families. Finally, we show how to extend our definition to some generalized algebraic theories that are not finitely presented, such as the theory of contextual cwfs.