Practical Foundations of Mathematics

Paul Taylor

8.2  The Category of Contexts

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

Cn(G) = {(Y,J)|G,Y \vdash J}
represents the context G, where we shall use J for the right hand side of an arbitrary judgement. The structural rules translate elements of one such set to another: they define an action on Cn(-) which is essentially the Cayley-Yoneda action introduced in Section 4.2. This satisfies the laws of the Extended Substitution Lemma (Proposition 1.1.12).

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

omitted vchbox environment               omitted vchbox environment
where (following Convention 1.1.8) the variable name x does not already occur in G. It is what we use at the beginning of a function definition ( ), universal proof (" ) or, without a variable, implication ( ).

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

omitted prooftree environment
With the axiom for the empty context ([  ] = [  ]) we have all the rules for the additional forms of judgement for formation and equality of contexts, because reflexivity, symmetry and transitivity are derivable from those of type equality, and hence equality of substitution (into a type-symbol). Briefly, contexts are well formed and equal iff the corresponding types are, in the preceding context, and the variable names agree.

This satisfies

G = D Cn(G) = Cn(D), because the rule

omitted prooftree environment
is derivable, by inserting coercion rules (Definition  8.1.7(c)).

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

omitted prooftree environment
is derivable: Remark 8.2.8 gives a canonical isomorphism between any two contexts which differ only in these names (open a-equivalence).

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,

omitted prooftree environment
but this is also sufficient.

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

omitted prooftree environment
ie the addition of an unused variable at any valid position in a context, but by the permutations above it may be taken to be the last. This rule was given in Definitions 1.4.8 and Remark  2.3.8 for propositions and for types, respectively.

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

{(Y,J)|G,Y\vdash J} {(Y,J)|G,x:X,Y\vdash J},
and we abstract this as (the contravariant action of) a display map:
omitted prooftree environment
The hat was introduced in Notation 1.1.11 and used in Sections 1.5, 2.3 and  4.3. Display maps are marked with open triangle arrowheads. The composite of zero or more displays will be indicated by a double triangle arrowhead ( [abut]) and [^(Y)] . The subscript on [^(x)]Y refers to the extension Y of the context G in which [^(x)] is defined.

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.


DEFINITION 8.2.6 The cut rule is

omitted prooftree environment
Like coercion and weakening, it is a derived rule, because all of the rules are invariant under substitution.

Cut acts on terms, types, judgements and derivations by substitution,

(Y,J) (Y[x: = a],J[x: = a]),
ie [x: = a]:Cn([G,x:X]) Cn(G) by J(x) J(a).

The associated generating map is of the form

omitted prooftree environment
which Definition 8.3.2 characterises semantically .

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

omitted prooftree environment
where, by the first cut, Y[x: = a] is a well formed type in the context G# and we abbreviate Y = Y[x: = a]. Similarly Y = Y[x: = a][y: = b].

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

[G,Y] =
G, ^
Y[y: = b]
 [y: = b [G, y:Y, ^
Y] [^(y)] [G,Y]
is the identity, but to show that this is well formed we need the version without Y first.

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 prooftree environment        omitted prooftree environment
Of course [y: = x] is a section of the display [^(y)], but its composite with [^(x)] performs renaming, so the parallel pairs make [G,x:X] [G,y:X]:
omitted diagram environment (R)
Again this simpler law, applied to Y and with x FV(F), is needed to show that the general case is well formed.

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

objects are contexts [G,F] extending G, so that the structure map [^(F)] :[G,F] G is always a composite of displays, and

morphisms [G,F] [G,D] are generated by displays and cuts which leave the context G untouched, subject to the laws above.

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