In the mathematical vernacular (Section 1.6), let and suppose introduce hypothetical things and properties. Formally, they expand the context in the sequent style, or open nested boxes in the box presentation. Things introduced by ``let'' are denoted by typed variables. Hypothetical properties may of course depend on entities which have already been introduced in the argument; now the types of the variables may also be dependent on what has gone before. This means that, as a precondition of opening the box or expanding the context, these types must themselves be shown to be well formed.
DEFINITION 8.1.1 The steps in an argument are called judgements. Amongst the direct algebraic steps (those within a fixed context G), we distinguish the following forms:
G\vdash f = y): that these propositions or types are intensionally equal.
For the postulates at the beginning of an argument we need
|
We discuss context formation in the next section, where it will become clear that we must also say when two contexts are equal, using equality of their types. The provision of arguments of types and operation-symbols also needs formation and equality rules for substitutions.
The idioms which close boxes or make the contexts smaller arise from the quantifiers (Remark 9.1.6 and the whole of the final chapter). For the time being, therefore, boxes never get closed. Despite the boxes and sequents, this chapter generalises, not the predicate calculus as we saw it in Sections 1.4- 1.5, but just resolution of Horn clauses involving atomic predicates, as in PROLOG (Remark 1.7.2ff).
At the algebraic level the only distinction between the behaviour of types and propositions is that elements (terms) of the same set (type) are distinguished , but proofs are anonymous. By giving names to the Horn clauses, proof-terms may be assigned to propositions (Remark 6.2.10); the main point of Section 2.4 was to do the same for implicational logic, using l-terms. Alternatively, we may simply assert that any two proofs of the same proposition in the same context are equal.
The classification of judgements also applies to the rules which justify them. These are the subject of the rest of this section.
Terms In this chapter, a term is an algebraic expression: just as in Definition 1.1.3, it is either a variable x belonging to the context, or an operation-symbol r applied to (zero or more) sub-terms.
REMARK 8.1.2 Let r be an operation-symbol, from the object-theory. It is applied to arguments,
|
omitted proofbox environment
and so on (with intermediate steps). The operation-symbol r might for example be composition, the types being the set of objects and hom-sets of a category. For propositions r names a Horn clause:
|
|
|
A lot of work remains to be done in the next section to define general substitutions u and their action u*t on terms - the calculus is highly recursive, and we have to break into the circle somewhere - but, in anticipation of this, here are the first of the formal rules.
DEFINITION 8.1.3 The term-formation rules are as follows:
|
|
Both of these rules incorporate weakening, cf Definition 1.4.8 and Remark 2.3.8. We study the structural rules in the next section.
Equality of terms The notion of equality needed in the foundations of dependent type theory is that from algebra: congruence. The judgement G\vdash a = b means that, for any valid judgement G,Y\vdash J in which a is a sub-expression, replacing it with b gives another valid judgement.
DEFINITION 8.1.4 The intensional term-equality rules are:
|
|
|
The anonymity of proofs is expressed by an indiscriminate equality rule:
|
REMARK 8.1.5 Intensional equality G\vdash a = b:X remains at the level of judgements: it does not (within the basic calculus) provide us with a term of some propositional type eq[a,b]. We discuss extensional equality briefly in Section 8.3. If we want to do something conditionally on the equality of a and b, it is extensional equality that we need.
Dependent types The dependency of types on terms (in predicates, hom-sets, arities, etc ) is expressed in a similar way to the application of operation-symbols to arguments, but there are no type variables.
DEFINITION 8.1.6 The direct type formation rule is
|
|
Equality of types The instantiation of a dependent type Y[[(x)\vec]] at equal terms [(a)\vec] = [(b)\vec] gives rise to equal types. We have not addressed this phenomenon before - indeed we have gone to some lengths to exclude it - but how can we deny that Factors[9×4] = Factors[6×6]? There must at least be a canonical isomorphism between the two, but if we chose to make this explicit we would be obliged to introduce formation and equality rules for it, which would have to obey further coherence rules with respect to other substitutions. Predicates at equal subjects also give rise to equal types; again there is a canonical way of translating a proof of one into a proof of the other, which must also obey coherence.
Rather than enter this labyrinth, we accept that types can be intensionally equal, ie if they have a common history of formation. Whereas set theory allows independently given types to be tested for equality or inequality, we do not. Section 9.2, however, does look at some of the categorical consequences of replacing equality by isomorphism .
DEFINITION 8.1.7 The type equality rules are
|
|
|
|
For the sake of giving a little more thought to the all-important coercion rule, we pause to consider its one-way version.
REMARK 8.1.8 Subtyping generalises equality between types to a non- symmetric relation(-judgement) G\vdash U Ì X satisfying
|
|
Subtyping also arises in object-oriented programming languages, in which complex types are developed from simpler ones by the addition of constructors and properties. As a mathematical analogy to this style, we may define a field as an Abelian group, with multiplication as an extra operation and the field axioms as extra conditions.
Terms of the narrower type inherit the covariant properties (positive, in the sense of Remark 1.5.9) associated with the wider one to which we coerce them; negative properties pass the other way. The coercion functions, like forgetful functors, need not be injective, but if they are suppressed from the notation then there must be at most one between any two types. (This has non-trivial consequences for function-types.)
REMARK 8.1.9 Some authors allow axioms stating equality of types, so that Heyting semilattices can be treated in the same framework. We forbid them, because interchangeability of objects should be expressed as isomorphisms, ie by means of two operation-symbols and two laws between their composites ( cf Section 7.6). See Exercise 4.7 regarding the quotient of a category by a system of canonical isomorphisms. As we commented before Proposition 3.2.11, the antisymmetry law for posets is a side-effect of the imposition of algebraic notation (Ù, Ú, Þ ), and is not an intrinsic feature of logic.
The restriction drastically simplifies the issue of type equality, as type- expressions can be equal only as a result of making equal substitutions into the same ``outermost'' type-symbol. This is essential to the validity of the structural recursion used in the interpretation (Section 8.4).
Definitional equality need not be excluded: it is of course very useful to define R = {(L,U):P(Q)|¼} as in Remark 2.1.1. This is harmless to the interpretation of dependent type theory, as we may simply replace the left hand side of the definition by the right. Inter-provability as a notion of equality of propositions will be discussed in Remark 9.5.6.
The object-language The pure theory cannot prove the existence of anything apart from the empty context [ ], so an object-theory is needed. As in simply typed algebra, it has types, operation-symbols and laws.
DEFINITION 8.1.10 A generalised algebraic theory L is given by
In order to give meaning to the ``contexts'' which occur in these data, we have to generate a small part of the language - as we did to state laws for an algebraic theory in Section 4.6. However, the ubiquitous dependencies must not be allowed to become circular, so we require that
the types and operation-symbols which occur in D must have been declared in advance.
Abstractly, the presentation defines a relation between each new symbol being defined and the type-symbols and operation-symbols that are used in the formation of its defining context D (there are operation- symbols in the terms that are the arguments of the type-expressions). This relation must be well founded.
DEFINITION 8.1.11 A stratified algebraic theory is one which obeys a stronger well- foundedness condition, that all of the operation-symbols r:X and laws a = b:X must be declared before variables x:X may be used as arguments of further type-symbols Y[x]. We shall not impose this condition in this chapter, as it is violated by the canonical language in Definition 8.4.6. See Exercises 8.1- 8.5 and Examples 9.2.4.
EXAMPLE 8.1.12 The theory of categories, with cm(f,g) for f;g.
omitted eqnarray* environment
In Remark 4.1.10 we said that the maps of a category C with O = obC could be collected together and presented by src,tgt:(mor C)® OxO instead of using the dependent type H[x,y]. In fact src,tgt will serve as the display map [^(f)] that corresponds to this dependent type, which we introduce syntactically and semantically in the next two sections.
omitted diagram environment
Before composition can be defined, its support - the set of composable pairs (f,g) with tgt(f) = src(g) - must be constructed. There is a natural syntactic description of this set, namely the context of the rule which introduces c. It is also the pullback of tgt and src, as marked in the diagram above, cf transitivity of a kernel pair (Proposition 5.6.4).
This chapter shows how to translate between the symbolic and diagrammatic idioms. The next section constructs the classifying category for L, ie the category in which this diagram is drawn, and shows that squares like the one marked really are pullbacks. In fact pullback performs all of the substitutions u* in Definitions 8.1.3(a), 8.1.4(c), 8.1.6 and elsewhere. In Section 8.4 we shall give the interpretation of the language, for which we shall need a sharper form of the induction which generates it.