Now we shall interpret the language in a category with displays, and show that any such category arises up to equivalence as Cn^{×}_{L} for some generalised algebraic theory L, as we did in Sections 4.6 and 7.6.
Derivation histories in normal form Before giving the interpretation itself we must clarify the well founded structure over which it is defined, because Example 8.2.1 shows that this is delicate. We must take (equivalence classes of) histories, rather than the strings of operation symbols and variables, as the terms etc in \Clone_{L}^{x}.
REMARK 8.4.1 The rules of Section 8.1 may be reorganised according to the use they make of the objectlanguage (Definition 8.1.10). Let u:G® D be any morphism (substitution), [G,Y] an extended context and x a variable which is not in G, D or Y.
In the presentation of the syntax these were listed under different headings (8.1.6, 8.2.2, 8.2.5, 8.2.8 and 8.1.3(b) respectively), but they are obtainable from one another immediately, ie by the use of a single rule of derivation. Types are equal ( 8.1.7) iff they result from equal substitutions into the same typesymbol; similarly with context equality and coercion (8.2.3). omitted diagram environment These are all aspects of the same thing, for which it is convenient to take the display [^(x)]:[D,x:X]® D as the primitive form. The other, substituted, forms are obtained from the display by pullback.
(Definitions 8.1.3(a) and 8.2.6). We shall use the section [x: = r] of \nearrow ^{*}[^(x)] as the primitive form of the operation symbol. omitted diagram environment
REMARK 8.4.2 The typical formation step is therefore simply

To show that a context G º [[(x)\vec]:[(X)\vec]] is well formed we must prove


Comparing this with the recursive paradigm (Definition 2.5.1 and Section 6.2), the subexpressions to be considered in practice are the types of the context G and the terms used in the substitution u:G® D. The latter are the arguments of the type and operationsymbols as presented informally in Section 8.1. The wellfoundedness condition mentioned in Definition 8.1.10 is needed for the existence of derivations.
THEOREM 8.4.3 This is the normal form for derivations.
PROOF: We have shown throughout Remark 8.4.1 how the rules (for the generalised algebraic fragment) set out informally in Section 8.1 fit into the normal form. Weakening and cut (Definitions 8.2.5ff) commute with the last rule in the normal form, increasing the height of the derivation history by at most that of the substituted term, so histories are strongly normalising. []
The induction in this and later results is over the derivation tree, not just on the number of variables in G, since the target D of u may be a longer context than G. This allows for the possibility that nested operationsymbols may have greater arity than the outermost one. The base case is the empty context [ ].
In Section 7.4 we found the free model for equational algebraic theories with many but simple types as the quotient of the associated absolutely free model by the congruence generated by the laws. Because of the effect the laws have on types, this is not possible in the dependent case. We have to generate the well formed instances of equality as syntactic entities in themselves, along with the types, terms, contexts and substitutions, allowing coercions arising from such equalities. At the end these will form a congruence, and the terms may finally be treated as equivalence classes. The derivation histories form a recursive cover (Definition 6.2.2), but there is no canonical choice of history for any given term or type.
Interpretation To present the data for a model of a simply typed algebraic theory in Definition 4.6.2, we needed only each object \typeA_{X} itself which was to be the denotation of the sort X, together with some products of these objects to serve as the sources of the denotations of the operationsymbols. The dependent type situation is much more complicated. Now, for the sort D\vdash X, the object \typeA_{X} is the source of some semantic display map whose target is the interpretation [[D]] . We must begin the proof of the following theorem, ie the construction of [[]]:Cn^{×}_{L}® S by structural recursion, before completing its statement.
THEOREM 8.4.4 Let L be a generalised algebraic theory and let C be a category with a display structure D. Then the interpretations of L correspond bijectively to functors Cn^{×}_{L}® C¯ 1® C which preserve displays and the P and S pullbacks. The choice of pullbacks of displays defines the interpretation up to equality. Homomorphisms correspond to natural transformations as in Example 4.8.2(e).
PROOF: Using structural recursion over the derivations in Remark 8.4.2 the interpretation given in Remark 4.6.5 extends to dependent types:
COROLLARY 8.4.5 To interpret a particular context, type, term or morphism only finitely many choices of pullback are used. Hence such fragmentary interpretations exist even when no global choice of pullbacks is provided, and are unique up to unique isomorphism ( cf the proof of Theorem 7.6.9(b)). Also, when the interpretation of a type in a context has been chosen, the meaning of its terms is fixed up to equality. []
Canonical language Conversely, we shall show that every category with a rooted class of displays is equivalent to the category of contexts and substitutions for some generalised algebraic theory. This may be read off from the sketch in Proposition 8.3.11, but we need encoding operations (Section 7.6) to say that the P and S squares are pullbacks. As in Sections 4.2, 7.6 and 8.3, we shall temporarily use Greek letters for maps of C, the semantic category. German letters still denote syntactic morphisms. We shall not make a notational distinction between the objects of C¯ 1 and the typesymbols and contexts which they name; type expressions are flagged by the presence of a substitution action.
DEFINITION 8.4.6 Let C be a small category with a class of displays D. The canonical language L(C,D) is the following theory:
More precisely, each sequence F of displays, ie each object of C¯ 1,


Remark 8.4.1(a) put no restriction on the defining context D of a typesymbol: its types could be any substitution instances. Here we only introduce typesymbols in contexts which themselves consist of type symbols alone. Since no substitution operations are used, no pullbacks are needed to construct the interpretation of these contexts and typesymbols in C; in fact we recover [[\qq F]] = F.
