We have presented the formation and equality rules for terms and types using generalised substitutions u:G® D. These form a category, which is generated by the structural rules (weakening and cut) subject to the laws for substitution. This presentation is an elementary sketch: it is the culmination of the approach to semantics of formal languages which we began in Section 4.2. As we have some heavy symbol-pushing to do, the diagrammatically minded reader may find it helpful to read the next section first, as it presents the corresponding semantic arguments.
If you prefer symbols, remember that commutative diagrams simply show the types of the symbols. Giving a list of successively equal terms does not show the type information (which, after all, is what dependent type theory is all about), and makes it difficult to follow the reduction rules. In view of the fact that types contain terms as sub-expressions, the practice of annotating terms with their types is inadequate:
EXAMPLE 8.2.1 f:H[src(f),tgt(f)].
After defining equality of contexts we discuss the structural rules. These are derived in the sense that if the premise is deducible using the rules of the previous section then so is the conclusion. It is left to the reader to demonstrate this. The calculus has a ``term model'' in which
|
We write x Î G to mean that x:X is one of the variables which are listed in this context. Note that for a context G, if x Î FV(Y) for the type (expression) Y of one of the variables y Î G then x Î G itself. However, for a context extension [G,Y] we write x Î FV(Y) if x Î FV(Y) for some type in Y, where x may belong to G rather than Y ( cf Exercise 1.12).
Objects As before, these are contexts, but type dependency means that the class of well formed contexts must be defined recursively. Indeed the terms, types and contexts must be generated in a single simultaneous process (as remarked in Section 6.2). The starting point is the empty context [ ], which will be interpreted as the terminal object 1, but we shall find that a general context G is always present in the background.
DEFINITION 8.2.2 The hypothesis or context formation rule is
|
The objects and maps of the category will be contexts and multiple substitutions. Morphisms may only compose if the target of one matches the source of the other, ie they are equal objects of the category. This means we have to give rules defining equality of contexts which allow substitution of a term of one type for a variable of an equal type. These simply extend the type equality rules (Definition 8.1.7).
DEFINITION 8.2.3 The context equality rule is
|
This satisfies
G = DÞ Cn(G) = Cn(D), because the rule
|
REMARK 8.2.4 Our convention is to retain the variable names - in the analogy of Remark 4.3.14, we use coloured wires where, eg , [Pit95] numbers the pins. In accounts of the latter kind, [G,x:X] and [G,y:X] are equal contexts. Nevertheless for us the rule
|
Coloured wires, unlike numbered pins, may be permuted, but now our freedom to do this is restricted by the type dependency. Of course, it is necessary that the two types be well formed in the same context,
|
It would be nice to treat permutation as equality. A context would be no longer a list but a partially ordered set, subject to the order relation implicit in Definition 1.5.4, namely that the variables occurring freely in any type must be mentioned before it in the listing of the context.
Unfortunately the explicit listing is required for the semantics, since, even in a category with specified products (or pullbacks), the choice usually cannot be made commutatively or associatively (Remark 8.3.1). Contexts which differ only by permutation are nevertheless canonically isomorphic, by a substitution which is the identity on each variable. They also share the same clone, so to make the isomorphism explicit the order of the variables must be specified.
Display maps As in Definition 4.3.11(b), the arrow class is generated by display maps and single substitutions. The former arise from
DEFINITION 8.2.5 The weakening rule is
|
Weakening, like coercion, is a derived rule, since in all of the rules of the previous section variables may be added to the context. Indeed only Definition 8.1.3(b) mentioned the context at all, but we added passive G and Y to it to incorporate weakening.
The action on clones is the inclusion [^(x)]*:Cn(G)\hookrightarrow Cn([G,x:X]) since
|
|
Cuts The other class of generating maps consists of the substitutions of one term for a variable of the same type in the same context. As the types may now have free variables, Definition 1.1.10 must be extended to deal with substitution of terms into types and contexts. This is routine, but once again we see the need for type-equality rules.
1
DEFINITION 8.2.6 The cut rule is
|
Cut acts on terms, types, judgements and derivations by substitution,
|
The associated generating map is of the form
|
The context G of global parameters is needed in the cut rule in order to compose cuts. Let G\vdash X type and G,x:X\vdash Y type; then
|
Notice that the double substitution is by [y: = b];[x: = a] in that order.
Laws In the Extended Substitution Lemma (Proposition 1.1.12) we must now say whether the variables x and y may or may not occur free in the type-expressions, as well as in the terms. In the following, y:Y is later in the context than x:X, and Y may in general depend on x.
REMARK 8.2.7 The variable y never occurs free, and x Ï FV(a,X).
omitted eqnarray* environment
The type Y may depend on x in ([^(S)]) but not in (\check S). We shall see in Lemma 8.2.10 that these laws play different roles , with opposite senses as reduction rules. In fact (\check S) may be derived (as an unoriented law) from ([^(S)]) and (R) .
Of course the object-language also contributes laws, but we shall regard them as part of the term calculus (so a denotes an equivalence class modulo such laws) rather than of the sketch for the category composed of substitutions.
Now that the types may be dependent it is essential to include them in the statement of the laws. We must in particular ensure that the terms and the intermediate types are well formed. As usual, commutative diagrams provide the clearest mode of expression; the little arrows in the corners of the squares indicate the sense of the reduction rules.
The general forms of the laws, which we shall mark with a star, allow for an extension Y to the context which may depend on y. For example the general form of (T*) is that the composite
|
Similarly we have to know that [^(y)]*[^(x)]*Y = [^(x)]*[^(y)]*Y for
omitted diagram environment
The following diagrams show how the (S*) and (W*) laws including the context extension Y reduce to the simpler forms, where PP and [^(SS)] stand for as many squares as there are variables in Y.
omitted diagram environment
quote omitted diagram environment
The (W*) law is the Substitution Lemma itself:
omitted diagram environment
REMARK 8.2.8 The final law justifies renaming and permutation ( exchange) of variables. It uses contraction, ie the special case of cut where the term is a new variable of the same type:
|
|
omitted diagram environment
Hence the renaming and exchange rules (Remark 8.2.4) are derivable, since we have shown how to turn x into y and move it past F (which may be empty). []
Normal forms for morphisms We shall now prove Theorem 4.3.9 and Corollary 4.3.13 for dependent types: each map in the category can be written uniquely as a multiple substitution in a certain normal form. As usual the most natural way of expressing this involves a ground context G. Essentially, this corresponds to the slice category Cn×L¯ G (Definition 5.1.8), but the appropriate notion is actually a full subcategory, cf \SubC(X) Ì C¯ X (Remark 5.2.5), which is the slice relative to monos.
DEFINITION 8.2.9 The relative slice Cn×L¯ G is the category whose
By Exercise 8.9, such maps are exactly the commutative triangles
omitted diagram environment
LEMMA 8.2.10 Any map u:[G,F]® [G,D] in Cn×L¯ G may be expressed uniquely (up to the choice of new names D¢) in the form
omitted diagram environment
quote omitted eqnarray* environment