Practical Foundations of Mathematics

Paul Taylor

8.4 Interpretation

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 object-language (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.

(a)

Each type-symbol (D\vdash X type) Î L provides the following features:

the type-expression G\vdash u^*X, whose arguments are given by the components of u,
the extended context [G,x:u^*X,Y],
weakening [^(x)]_Y :[G,x:u^*X,Y]Ž [ G,Y],
contraction [x˘: = x]_Y :[G,x:u^*X,Y]Ž [G,x:u^*X,x˘:u^*X,Y],
and the variable G,x:u^*X,Y\vdash x:u^* X qua term.

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 type-symbol; 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.

(b)

The type of an operation-symbol may in general be a substitution instance \nearrow ^*X of a type-symbol, given by the previous part. Each operation-symbol (D\vdash r:\nearrow ^*X) Î L provides

the term G,Y\vdash u^*r:(u;\nearrow )^*X and
the cut [x: = u^*r]_Y :[G,Y[x: = u^*r]] Ž [G,x:(u;\nearrow )^*X,Y]

(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

(c)

Each law (D\vdash f^*r = g^*s:h^*X) Î L, where h = f;\nearrow = g;q, relates two terms of the same type (Definition 8.1.4(a)); omitted diagram environment it extends to G,Y\vdash (u;f)^*r = (u;g )^*s:(u;h)^*X (congruence, 8.1.4(c)), but there is insufficient space to show this.

(d)

The (reflexive, symmetric and) transitive laws of term equality are also needed (8.1.4(b)), as are the substitution laws (8.1.4(c) and 8.2.7). All of them feature in these diagrams, apart from (R), which disappears along with the variables in the interpretation anyway.

(e)

Type and context equality and coercion are derivable.

REMARK 8.4.2 The typical formation step is therefore simply

omitted prooftree environment

where J is a type-symbol, operation-symbol or law, cf the generalised cut rule (Definition 8.2.13). (If we laid out the derivation as a tree in the way suggested by this rule there would be a great deal of redundancy; the box style is more natural.)

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

x₁:\typeX₁,ź,x_n-1:\typeX_n-1\vdash \typeX_n type (n Ł len(G)).

Similarly, for a map u ş [[(y)\vec]: = [(a)\vec]] in the form of Remark 8.2.12(a) we need

omitted prooftree environment

where | ş [y₁: = \arga₁,ź,y_n-1: = \arga_n-1]: GŽ D˘ ş [y₁:\typeY₁,ź,y_n-1:\typeY_n-1] , \arga_n ş f^*r and \typeY_n ş g^*Y. We have to prove commutativity of the square, ie that the maps are composable and their composites are equal, in order to justify the typing. This uses the laws (which must be part of the derivation tree) and the normal form theorem (Lemma 8.2.10): the derivations are of raw terms, but the justification of such formations may rely on certain laws, the two sides of which themselves each require derivation sub-trees.

Comparing this with the recursive paradigm (Definition 2.5.1 and Section 6.2), the sub-expressions 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 operation-symbols as presented informally in Section 8.1. The well-foundedness 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 operation-symbols 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 operation-symbols. 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:

(a): The base case is the empty context [ ], which is interpreted as the terminal object 1 of C.
(b): The (displays corresponding to) type-symbols D\vdash X type are given.
(c): Substitution along u:GŽ D and [^(Y)] :[G,Y]Ž G uses the chosen P and S pullbacks of display maps against arbitrary maps in C; cut and weakening are sound.
(d): The (sections of displays corresponding to) operations are given.
(e): The laws of L are given. Any provable equality has a derivation tree, by induction over which the terms have equal interpretations.
(f): The laws T, P, S, W and R (the Extended Substitution Lemma) hold by Proposition 8.3.11. []

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 type-symbols 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:

(a)

Essentially, each display map XŽ D gives a type-symbol which we shall call just X (though this is an abuse of notation).

More precisely, each sequence F of displays, ie each object of CŻ 1,

1 Ź \typeX₁ Ź \typeX₂ Ź ···Ź \typeX_n Ź \typeX_n+1,

names a context-symbol

\qq F ş [x₁:\typeX₁,x₂:\typeX₂,ź, x_n:\typeX_n,x_n+1:\typeX_n+1],

in which all of the types are type- symbols with arguments exactly the preceding variables. The variable names are chosen arbitrarily.

Remark 8.4.1(a) put no restriction on the defining context D of a type-symbol: its types could be any substitution instances. Here we only introduce type-symbols 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 type-symbols in C; in fact we recover [[\qq F]] = F.

There are two classes of operation-symbols.

(b)

Each section of a display names an operation-symbol:

DŽ ^a
Ź X D \vdash \qq a:X