On generalized algebraic theories and categories with families

Marc Bezem, Thierry Coquand, Peter Dybjer, Martin Escardo

Research output: Contribution to journalArticlepeer-review

70 Downloads (Pure)

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.
Original languageEnglish
Number of pages18
JournalMathematical Structures in Computer Science
Early online date18 Oct 2021
DOIs
Publication statusE-pub ahead of print - 18 Oct 2021

Keywords

  • Dependent type theory
  • generalized algebraic theory
  • category with families
  • initial model
  • internal category
  • Martin-Löf type theory

Fingerprint

Dive into the research topics of 'On generalized algebraic theories and categories with families'. Together they form a unique fingerprint.

Cite this