nLab generalized algebraic theory

Idea

A generalized algebraic theory (GAT, Cartmell 1978/86) is a dependent type theory in the syntactic sense: There are judgments declaring types and terms of types, where, critically, a type $A$ declared in context $\Gamma$ is allowed to depend on terms of $\Gamma$. The only other judgments allowed are of equality (judgemental equality) of pairs of types or terms.

Cartmell 1978/86 introduced the notion of contextual category alongside that of generalized algebraic theories (GATs), specifically to provide the latter with a functorial semantics. He proved that the contextual category generated by a GAT (its syntactic category) is its initial model, taking an early step in understanding the categorical semantics of dependent type theory.

The latter program has more generally dealt with complicated coherence issues that arise for richer kinds of contextual categories, corresponding to type theories admitting further type formation inference rules such as for dependent product types (“$\Pi$-types”), for identification types (“Id-types”), and so on. The key distinction is that a plain GAT cannot use a judgment of the form “$A$ is a type in context $\Gamma$” as a premise, and hence cannot express general dependent type-formation rules.

The basic target for categorical semantics of a GAT is the contextual category of families of (families of families of…) sets, which avoids some coherence issues via stratifying its objects by their number of layers of families. Much of the difficulty in providing categorical semantics for dependent type theory is in understanding how to transfer such models to the ordinary category of sets, other locally cartesian closed categories and beyond.

Examples

The theory of categories is a GAT:

1. Its type judgments are that $\mathrm{Ob}$ is a type and that, in the context of two terms $a,b:\mathrm{Ob},$ we have that $\mathrm{Hom}(a,b)$ is a type.

2. Its term judgments are that $\mathrm{id}(x):\mathrm{Hom}(x,x)$ in context $x:\mathrm{Ob}$ and that $g\circ f:\mathrm{Hom}(x,z)$ in context $x,y,z:\mathrm{Ob},f:\mathrm{Hom}(x,y),g:\mathrm{Hom}(y,z).$

3. Its equations are those imposing associativity and unitality, as usual.

One can also directly axiomatize the theory of monoidal categories by adding:

1. A term $I$ of sort $\mathrm{Ob},$ in the empty context.

2. Terms $a\otimes b:\mathrm{Ob}$ in context $a,b:\mathrm{Ob}.$

3. Similarly, terms $f\otimes g:\mathrm{Hom}(x\otimes y,z\otimes w)$ in the appropriate context, as well as for the unitors and the associators.

4. Additional equations corresponding to the pentagon and triangle diagrams, functoriality of $\otimes$, and inverse+naturality squares for remaining operations.

The axiomatization of strict monoidal categories is similar, but briefer.

The theory of 2-categories is also a GAT, and adds types $2-\mathrm{Hom}(f,g)$ in context $x,y:\mathrm{Ob},f,g:\mathrm{Hom}(x,y).$ This and further higher-categorical examples illustrate the need for iterated families of sets in the models.

Finally, multicategories form a GAT with infinitely many type and term formation rules, namely that we have a type $\mathrm{Ob}$ and, for every $n,$ a type $\mathrm{Hom}(x_1,\ldots,x_n;y)$ in context $x_1,\ldots,x_n:\mathrm{Ob}.$ We must, similarly, axiomatize all the composition operations of different arities separately.

Relationship to Many-Sorted Algebraic Theories

A many-sorted algebraic theory is a GAT with no nontrivially dependent types.

Relationship to Essentially Algebraic Theories

Cartmell’s paper explains how for every GAT there is an essentially algebraic theory (EAT) with the same models and for every EAT there is a GAT with the same models in the category of sets, up to the coherence issues in moving between the categories of sets and of families of sets mentioned above.

Related concepts

• initiality conjecture
• Martin-Löf dependent type theory

References

• John Cartmell, Generalised Algebraic Theories and Contextual Categories, PhD thesis, Oxford University (1978) [pdf]

• John Cartmell, Generalised Algebraic Theories and Contextual Categories, Annals of Pure and Applied Logic, 32 (1986) 209-243 [doi:10.1016/0168-0072(86)90053-9]