Generalized Algebraic Theories

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

A many-sorted signature declares a set of sorts and, for each operation symbol, a list of argument sorts and a result sort. Try to declare a category. There are two sorts, $\mathrm{Ob}$ and $\mathrm{Ar}$, and an operation $$\mathrm{comp}:(\mathrm{Ar},\mathrm{Ar})\to \mathrm{Ar}.$$ This declaration is well formed and wrong: it composes any two arrows. The usual repair adds $\mathrm{dom},\mathrm{cod}:\mathrm{Ar}\to \mathrm{Ob}$ and the equations $\mathrm{dom}(\mathrm{comp}(f,g))=\mathrm{dom}(f)$ and so on, together with a side condition $\mathrm{cod}(f)=\mathrm{dom}(g)$; but a side condition is not part of a many-sorted signature, and adding it as an equation is impossible because the equation would have to be a premise of the declaration rather than an axiom about it.

What the mathematics wants is one sort for each pair of objects, so that the sort of the result depends on terms occurring in the sorts of the arguments. A signature that permits this is a generalized algebraic theory. The difficulty is not the notation, which is immediate, but the definition of what such a declaration is: the next section shows that sorts, operations and equations cannot be presented as three separate lists.

A signature that cannot be sorted into three lists

An ordering of the three kinds of declaration therefore cannot be imposed in advance: a sort may depend on an operation, an operation on an equation, and an equation on a sort. A presentation must be a single sequence in which each entry is checked against everything before it. That is the shape of definition 147.4, and it is why the definition proceeds by induction on the length of the sequence rather than by describing three sets.

Two further decisions are forced. First, “everything before it” must be made precise without a syntax, since a syntax is what the theory is supposed to generate; the device is to interpret a partial presentation as a category of models and each declaration as an operation available uniformly in every model. Second, the ambient notion of model must already support contexts, dependent types, terms and substitution. That is exactly a category with families (definition 54.16), and the strict morphisms of definition 54.26 are what “uniformly” will mean.

Uniform families and presentations

Uniformity is a condition on the whole category of models at once. It replaces the syntactic notion “an expression in the vocabulary declared so far”: an expression would give such a family by interpretation, and the definition takes the families themselves as primitive so that no syntax has to exist yet.

This is Definition 4 of Bezem, Coquand, Dybjer and Escardó, On generalized algebraic theories and categories with families, physical page 6 of the journal version. The definition is independent of any syntax: nothing in it mentions an expression.

Proof of Lemma 147.5 — Extensions carry uniform families forward

Proof. Let $F^{\prime }\in {\mathbf{CwF}}_{{\mathrm{\Theta }}^{\prime }}({\mathcal{C}}^{\prime },{\mathcal{D}}^{\prime })$. In each of the three extension cases of definition 147.4, $F^{\prime }$ is by construction a morphism $F:=U{F}^{\prime }$ of ${\mathbf{CwF}}_{\mathrm{\Theta }}$, possibly subject to one extra equation. Uniformity of $\mathrm{\Gamma }$ over ${\mathbf{CwF}}_{\mathrm{\Theta }}$ gives $F({\mathrm{\Gamma }}_{U{\mathcal{C}}^{\prime }})={\mathrm{\Gamma }}_{U{\mathcal{D}}^{\prime }}$, which is the required equation for $\mathrm{\Gamma }\circ U$ at $F^{\prime }$. The same argument applies verbatim to types and to terms, because in each case the required equation is $F^{\prime }(A_{U{\mathcal{C}}^{\prime }})=A_{U{\mathcal{D}}^{\prime }}$ and $F^{\prime }$ acts as $F$ on types and terms. ◻

Lemma 147.5 is what makes definition 147.4 well founded: the family used to justify entry $n+1$ must be uniform over ${\mathbf{CwF}}_{{\mathrm{\Theta }}_n}$, and every family available at stage $n$ is still available at stage $n+1$. It is used without comment in every calculation below.

The initial model

Definition 147.4 specifies a category of models without producing one. The syntactic construction produces the initial one, and it must be carried out entry by entry: theorem 54.27 builds the initial bare CwF, and each added sort, operator or equation changes the raw grammar, the inference rules and the quotient, so nothing about the extended theory follows from the bare statement.

Proof of Theorem 147.9 — Initiality

Proof. Induction on the length of $\mathrm{\Theta }$. At each stage the construction produces four items: a grammar for raw contexts, substitutions, types and terms; a system of rules generating four partial equivalence relations $$\mathrm{\Gamma }={\mathrm{\Gamma }}^{\prime },\mathrm{\Gamma }⊢A=A^{\prime },\mathrm{\Gamma }⊢\gamma ={\gamma }^{\prime }:\mathrm{\Delta },\mathrm{\Gamma }⊢a=a^{\prime }:A,$$ whose quotient is $T_{\mathrm{\Theta }}$; a proof that $T_{\mathrm{\Theta }}$ is an object of ${\mathbf{CwF}}_{\mathrm{\Theta }}$; and, for each object $\mathcal{C}$, an interpretation morphism $[[-{]]}_{\mathcal{C}}:T_{\mathrm{\Theta }}\to \mathcal{C}$ shown to be the only one.

Base. For $\mathrm{\Theta }=\varnothing$ the four items are theorem 54.27: the raw syntax of definition 54.2, its equality rules, the quotient CwF, and the unique strict morphism into any CwF.

Adding a sort $(\mathrm{\Gamma },S)$. Extend the grammar of raw types by one production $A::=S$ and the rules by $$\frac{}{{\mathrm{\Gamma }}_{T_{\mathrm{\Theta }}}⊢S}$$ where ${\mathrm{\Gamma }}_{T_{\mathrm{\Theta }}}$ is the value at $T_{\mathrm{\Theta }}$ of the uniform family $\mathrm{\Gamma }$. Neither the raw contexts, substitutions nor terms change, and no rule for the other three relations mentions $S$, so the partial equivalence relations extend conservatively: two raw types are related in the extension exactly when they are related in $T_{\mathrm{\Theta }}$ or both are $S$ in a context related to ${\mathrm{\Gamma }}_{T_{\mathrm{\Theta }}}$. Put $S_{T_{{\mathrm{\Theta }}^{\prime }}}:=[S]$ and $T_{{\mathrm{\Theta }}^{\prime }}:=(T_{\mathrm{\Theta }},[S])$, an object of ${\mathbf{CwF}}_{{\mathrm{\Theta }}^{\prime }}$. Given an object $(\mathcal{C},S_{\mathcal{C}})$, extend the interpretation by $[[S]]:=S_{\mathcal{C}}$. It is a morphism of ${\mathbf{CwF}}_{{\mathrm{\Theta }}^{\prime }}$ because the added equation $[[S_{T_{{\mathrm{\Theta }}^{\prime }}}]]=S_{\mathcal{C}}$ holds by definition, and it is unique because any morphism must satisfy that equation and agrees with $[[-]]$ elsewhere by initiality of $T_{\mathrm{\Theta }}$.

Adding an operator $(\mathrm{\Gamma },A,f)$. Extend the grammar of raw terms by $a::=f$ and the rules by $$\frac{}{{\mathrm{\Gamma }}_{T_{\mathrm{\Theta }}}⊢f:A_{T_{\mathrm{\Theta }}}},$$ put $f_{T_{{\mathrm{\Theta }}^{\prime }}}:=[f]$ and $T_{{\mathrm{\Theta }}^{\prime }}:=(T_{\mathrm{\Theta }},[f])$, and extend the interpretation by $[[f]]:=f_{\mathcal{C}}$. The three verifications are as in the previous case, with $\mathrm{Tm}$ in place of $\mathrm{Ty}$.

Adding an equation $(\mathrm{\Gamma },A,a,a^{\prime })$. The grammar is unchanged. Add the rule $$\frac{}{{\mathrm{\Gamma }}_{T_{\mathrm{\Theta }}}⊢a_{T_{\mathrm{\Theta }}}=a_{T_{\mathrm{\Theta }}}^{\prime }:A_{T_{\mathrm{\Theta }}}},$$ which enlarges the partial equivalence relations; $T_{{\mathrm{\Theta }}^{\prime }}$ is the quotient of the same raw syntax by the enlarged relations. It is an object of ${\mathbf{CwF}}_{{\mathrm{\Theta }}^{\prime }}$ because the added rule gives $[a_{T_{\mathrm{\Theta }}}]=[a_{T_{\mathrm{\Theta }}}^{\prime }]$. For the interpretation, define the same partial function on raw syntax as before and check that it respects the enlarged relations: the only new generator is the displayed rule, and $[[a_{T_{\mathrm{\Theta }}}]]=a_{\mathcal{C}}=a_{\mathcal{C}}^{\prime }=[[a_{T_{\mathrm{\Theta }}}^{\prime }]]$ because $\mathcal{C}$ is an object of ${\mathbf{CwF}}_{{\mathrm{\Theta }}^{\prime }}$, so the two sides have equal interpretations. The induced map on the new equivalence classes is a morphism, and it is unique because it agrees with the unique morphism out of $T_{\mathrm{\Theta }}$ on every class.

At each stage the added item was checked against the four requirements, so the induction is complete. ◻

Uniqueness at each stage used only one fact about the added entry: that a morphism of ${\mathbf{CwF}}_{{\mathrm{\Theta }}^{\prime }}$ is a morphism of ${\mathbf{CwF}}_{\mathrm{\Theta }}$ satisfying one further equation, which is definition 147.4 read off directly. Nothing was inherited from theorem 54.27 except the base case.

Proof of Corollary 147.10 — Uniform families are contexts of the initial model

Proof. A context ${\mathrm{\Gamma }}^{\prime }$ of $T_{\mathrm{\Theta }}$ gives a family whose value at $\mathcal{C}$ is $[[{\mathrm{\Gamma }}^{\prime }{]]}_{\mathcal{C}}$; it is uniform because for $F:\mathcal{C}\to \mathcal{D}$ the composite $F\circ [[-{]]}_{\mathcal{C}}$ is a morphism $T_{\mathrm{\Theta }}\to \mathcal{D}$, hence equals $[[-{]]}_{\mathcal{D}}$ by initiality, so $F([[{\mathrm{\Gamma }}^{\prime }{]]}_{\mathcal{C}})=[[{\mathrm{\Gamma }}^{\prime }{]]}_{\mathcal{D}}$. Conversely a uniform family $\mathrm{\Gamma }$ gives the context ${\mathrm{\Gamma }}_{T_{\mathrm{\Theta }}}$. One composite is the identity because $[[{\mathrm{\Gamma }}_{T_{\mathrm{\Theta }}}{]]}_{T_{\mathrm{\Theta }}}={\mathrm{\Gamma }}_{T_{\mathrm{\Theta }}}$, since $[[-{]]}_{T_{\mathrm{\Theta }}}$ is the identity by initiality; the other is the identity because uniformity applied to the morphism $[[-{]]}_{\mathcal{C}}:T_{\mathrm{\Theta }}\to \mathcal{C}$ gives $[[{\mathrm{\Gamma }}_{T_{\mathrm{\Theta }}}{]]}_{\mathcal{C}}={\mathrm{\Gamma }}_{\mathcal{C}}$. The arguments for types and terms replace “context” by “type over the corresponding context” and “term of the corresponding type”. ◻

Corollary 147.10 removes the largeness recorded in remark 147.8: a presentation may be rewritten so that each entry names a context, type and terms of the initial model constructed so far, and it then becomes a small syntactic object.

Proof of Theorem 147.11 — Structural induction

Proof. The inclusion $\iota :\mathcal{P}\to T_{\mathrm{\Theta }}$ is a strict CwF-morphism, by the closure conditions, and it preserves the $\mathrm{\Theta }$-structure by hypothesis; so $\mathcal{P}$ is an object of ${\mathbf{CwF}}_{\mathrm{\Theta }}$ and $\iota$ is a morphism of that category. The equations of $\mathrm{\Theta }$ hold in $\mathcal{P}$ because they hold in $T_{\mathrm{\Theta }}$ and $\iota$ is injective. By theorem 147.9 there is a unique $h:=[[-{]]}_{\mathcal{P}}:T_{\mathrm{\Theta }}\to \mathcal{P}$, and $\iota \circ h:T_{\mathrm{\Theta }}\to T_{\mathrm{\Theta }}$ is a morphism of ${\mathbf{CwF}}_{\mathrm{\Theta }}$, hence equal to the identity by initiality. So $\iota$ is surjective on each of the four kinds of datum. ◻

The hypotheses of theorem 147.11 are exactly the clauses of definition 54.16, definition 147.4; there is one closure condition per constructor of the raw syntax and one per declared symbol, and no condition for the declared equations, which hold automatically in a subclass of a model.

Cartmell’s first-order syntax

Cartmell’s original definition proceeds through a syntax: raw expressions, judgment forms $\mathrm{\Gamma }⊢A\text{type}$ and $\mathrm{\Gamma }⊢a:A$ together with the two equality judgments, and a presentation is a set of derivable declarations closed under those rules. Models are then contextual categories. The relationship to definition 147.4 at the exact strength supported here is the following, and no more.

Proof of Proposition 147.13 — Interpretation into the first-order account

Proof. Corollary 147.10 converts each uniform family into a datum of $T_{{\mathrm{\Theta }}_n}$ for the corresponding initial segment ${\mathrm{\Theta }}_n$, and by the construction in theorem 147.9 each such datum is the class of a raw expression derivable from the rules generated by ${\mathrm{\Theta }}_n$. The three shapes of entry in definition 147.4 produce the three displayed shapes of declaration, and none of them is an equation between types. ◻

Optional route.

Second-order signatures with binding $\star$

Every entry of definition 147.4 declares an operation whose arguments are terms. A binder is not of that shape. Writing the untyped lambda calculus as a signature, one wants $$\mathrm{Tm}:\text{sort},\mathrm{lam}:(\mathrm{Tm}\to \mathrm{Tm})\to \mathrm{Tm},-\cdot -:\mathrm{Tm}\to \mathrm{Tm}\to \mathrm{Tm},$$ with the equation $\mathrm{lam}(g)\cdot u=g(u)$. The declared type of $\mathrm{lam}$ mentions a function space $\mathrm{Tm}\to \mathrm{Tm}$ of the metatheory, so it is not first order and not strictly positive. The immediate consequence is that there is no usable notion of homomorphism: a map $\alpha$ between two such models would have to satisfy $\alpha ({\mathrm{lam}}_M(g))={\mathrm{lam}}_N(\alpha \circ g\circ ?)$, and nothing types the hole, because $\alpha$ runs in one direction only.

The repair is to add contexts and substitutions explicitly, index the sort of terms by contexts, and turn the metatheoretic function into a term in an extended context. Applied to the display above it produces a first-order presentation in the sense of definition 147.4.

Suggested first pass.

Begin with exercise 147.8 and exercise 147.9, then complete exercise 147.12.

Exercise 147.8¶

★☆☆ Write the presentation of reflexive graphs — one sort of vertices, one sort of edges indexed by two vertices, and one operation giving a loop at each vertex — and identify the uniform family of contexts used for the edge sort. Then say what an internal reflexive graph is in the CwF $\mathbf{Set}$.

Referenced from 3 locations

• Generalized Algebraic Theories

Exercise 147.9¶

★★☆ Prove directly, without corollary 147.10, that the family assigning to each CwF its chosen terminal object is uniform, and that the family assigning to each CwF some chosen non-terminal context is not. Which clause of definition 54.26 is responsible?

Referenced from 3 locations

• Generalized Algebraic Theories

Exercise 147.10¶

★★★ Give a Cartmell-style theory with a declaration $\mathrm{\Gamma }⊢A=A^{\prime }\text{type}$ that is not the image of any presentation under proposition 147.13, or prove that in the case you choose the type equation can be replaced by a term equation as in remark 147.14. State exactly which of the two you have established.

Referenced from 2 locations

• Generalized Algebraic Theories

Exercise 147.11¶

★★☆ Show that theorem 147.11 fails if the closure condition on comprehension is dropped: exhibit a presentation and a subclass of $T_{\mathrm{\Theta }}$ closed under everything except $-.-$ that does not contain every context.

Referenced from 2 locations

• Generalized Algebraic Theories

Exercise 147.12¶

★★★ Practical project.gat-presentation-checker Implement a checker for presentations in the small syntactic form supplied by corollary 147.10. The input is a finite list of entries. An entry is a sort declaration, an operator declaration, or an equation; in each case its context, type and terms are given as raw expressions over the CwF combinators of definition 54.16 extended by the symbols declared in earlier entries. The program processes the list in order and, for each entry, checks that its context is a derivable context, that its type is a derivable type over that context, and that its terms are derivable terms of that type, using only the rules generated by the entries already accepted.

Invariant. The program maintains, after entry $n$, exactly the set of symbols declared by ${\mathrm{\Theta }}_n$ and the equations declared by ${\mathrm{\Theta }}_n$, and it never uses a symbol or an equation from a later entry when checking an earlier one. It checks this by recording, with every accepted judgment, the index of the last entry used in its derivation, and by verifying that the index is smaller than the current one.

Concrete result. For each entry the program prints accepted together with two recorded indices — the last entry of any kind used, and the last equation used, or none — or rejected together with the reason: undeclared symbol, ill-typed argument, or an equation not yet available.

Acceptance test. Run it on the monoid presentation of example 147.6: all six entries must print accepted, and the last entry used by the left unit law must be the entry declaring $\ast$. Run it on the presentation of example 147.1 in the displayed order: all seven entries must be accepted; the last equation used by $W$ must be the entry declaring $x_0=x_1$, and the last entry of any kind used by $W$ must be the entry declaring $Z$. Reporting only one of those two indices is not enough, because $W$ depends on a sort declared after the equation. Run the list again with the equation moved after the declaration of $W$: the entry for $W$ must be rejected with the reason equation not yet available. A run that accepts the reordered list has failed to check the argument types of $Z$ against the equations available at that point, which is the precise defect this test detects.

Referenced from 3 locations

• Generalized Algebraic Theories