Mathematical reasoning in the large (as we have been doing it) involves the introduction and manipulation of symbols for individuals and structures which successively depend on one another. For example we may introduce a category C, some objects X and Y of C, a morphism f of the hom-set from X to Y, and (if C is a concrete category) elements of some pullback whose construction involves f. Similar idioms of presentation may be found in geometry, algebra, analysis and so on. Simple type theory (reasoning as we have studied it) does not allow for this dependency: we must consider more complicated calculi.
We studied propositions dependent on terms in Section 1.4, where they were called predicates (but type-theorists prefer the word proposition). The main story in a proof in the predicate calculus is told by the logical formulae which are asserted at each step. The proof boxes which we used in Sections 1.4-1.7 were designed to reflect this: variables were consigned to the margin, and we hardly mentioned types as they and any function-symbols which we used were understood to come from a simply typed algebraic theory (maybe even a free one).
A dependent-type proof is much busier, since we also have to show that the types and terms we use are well formed. This goes on in the same current of reasoning, attention passing amongst these different aspects. Nikolas de Bruijn devised ways of expressing successive dependencies in AUTOMATH, with various conventions for saying that the context of the previous line was to be repeated, augmented or diminished, or that the current line was asserted in a global or some other context. As before, here we shall use the box or sequent style according to the emphasis we wish to place on the changes of context.
For some authors, the phrase ``dependent type theory'' means the study of the universal quantifier " or dependent product P, which generalises the function-type ® . That is the subject of the final chapter: this one sets up the correspondence between type theory and category theory at the algebraic level. The symbolic rules and universal properties of the quantifiers are then directly related. If you wish to go straight to Chapter IX, you should just observe the way in which contexts are used as vertices of commutative diagrams, and that this notation is sometimes abbreviated to a juxtaposition of letters denoting contexts or types.
Examples of types dependent on terms that we have already met include the hom-set C[x,y] for two objects of any category, and the arity ar[r] of an operation-symbol in any infinitary free theory. In each of these cases, an alternative presentation mor C® (obC)2 or k® W is useful for some purposes (Remark 4.1.10 and Definition 6.1.1). The targets of these maps are the types of the independent variables, and the source is the disjoint union \coprodx Y[x], displaying the type Y[a] over its index a Î X. Diagrams (expressing limits or colimits) in categories may also be seen as dependent types, but the additional arrow information makes the situation more complicated : it is handled by the Grothendieck construction, Proposition 9.2.7.
The notion of generalised algebraic theory, ie with dependent types, is powerful enough to serve as a general meta-language. Not only is the theory of categories an example of it, but so is the theory of generalised algebraic theories itself, as are even stronger notions such as cartesian closed categories and toposes. ( Cf that a few basic styles of symbolic reasoning such as the ruled lines and sequent notation for deductions suffice to set out the rules of complex calculi.)
Although any practising mathematician can formulate any particular dependent-type argument quite fluently, a very complicated recursive construction is needed to describe the generality - which is what this chapter is about. After describing the calculus, we shall construct the classifying category using the techniques developed in Sections 4.2-4.6.
Recall that for simply typed algebraic theories this was a category with products; by Section 7.6 every such category arises in this way. The analogue for dependent types is a category with a class of display maps, such as k® W. Syntactically, displays drop one typed variable y:Y[[(x)\vec]] from a context [G,y:Y], whilst substitution of a term a for the variable x gives rise to a pullback square whose vertical maps are displays and which has the substitution morphism [x: = a] along the bottom. The class of displays must therefore be closed under pullback against any map.
According to set theory, the passage from a dependent type Y[x] to its display involves the axiom of replacement. Semantically, the general notation Y[x] is meaningless in itself: we understand it only via the interpretation of this syntax in terms of displays as given in this chapter, so the correspondence is the definition of Y[x], rather than a theorem or axiom. However, the particular case Y[n] = Tn(U) of a (possibly transfinitely) iterated functor does depend for its existence on a substantive axiom, as does the interpretation functor [[-]] (Section 9.6).
Earlier investigations of this subject made the perhaps more obvious generalisation from products to pullbacks (Remark 5.2.9). This is the extreme case of our formulation, in which arbitrary functions between sets play the role of displays. It has the effect of building equality types into the syntax, but this is not necessarily appropriate when the objects under study are computational (Proposition 8.3.4ff).
Our approach is based on a philosophical and idiomatic point to which John Cartmell [Car86] first drew attention. He called the relationship between [G,x:X] and G analytic in the sense of Immanuel Kant. For example, to speak of a ``sentence'' one must presuppose some particular language, since this is implicit in the nature of a sentence. By contrast, general functional relationships like ``the official language of a country'' are synthetic. The point of view we took in Remark 4.1.10 regarding the morphisms of a category was similarly based on the idea that when f and g compose it is not merely because tgtf = srcg accidentally.
Generalised algebraic theories can be interpreted in other categories besides sets. On the semantic side, the investigation of what morphisms may arise as displays can involve non-trivial issues in topology, order theory and other disciplines about which we shall just give a few hints in Section 8.3. Similarly, Chapter IX does some calculations about quantifiers and even the type of types.
This subject is very much in its infancy: it is notationally complicated, most algebraists concern themselves with simply typed theories such as groups, rings, modules, etc ., and logicians are more interested in the quantifiers. The account in this chapter is perhaps overly influenced by type theory (though the practitioners of that subject would, on the contrary, find it inadequate), as it allows for a high degree of interdependence amongst types. This is needed for comprehension ( cf Exercises 2.17 and 8.3ff) and for the equivalence with display categories.
There are, however, numerous examples from algebra whose dependency is ``stratified,'' with simply typed theories at each level (as in Section 4.6). We saw such a stratification in Sections 5.6 and 7.4 for the congruences for simply typed theories. Another is the theory of categories. This means that we must expect all of the difficulties associated with the category of categories (two-dimensional limits, pseudo-colimits, failure of regular epis to compose) to beset generalised algebraic theories too.
If the intended laws can be separated from the operation-symbols by stratification, then it is no longer a severe restriction to concentrate on free theories (with no laws within levels). Then there would a stratified theory of structural recursion, unification and resolution. All of these issues demand further research, but are beyond the scope of this book.
The aims of the present account are to identify how an object-theory contributes types, operation-symbols and laws to the language, and how the arguments are supplied by (the category composed of) substitutions. Section 8.2 describes this category, and Remark 8.4.1 the object-theory. Section 8.1 leads informally towards these from the vernacular.
Instead of defining the objects and maps of the category of contexts and substitutions directly, we do this by means of an elementary sketch as in Section 4.3. I began work on this chapter from the exercise of showing that the context-morphisms defined recursively in [Pit95] (essentially Remark 8.2.12) do indeed satisfy the axioms of a category. This proved to be unreasonably laborious, being a highly convoluted version of Proposition 2.7.5, and led me to the approach via sketches. This profoundly influenced the rewriting of Chapters IV and I.
It is well known that syntactic substitution is characterised by pullback, but Section 8.2 is probably the first explicit proof of this in a category fashioned directly from language. From this careful analysis we may determine what coherence conditions pullbacks along composites must satisfy, namely none so long as on-the-nose equalities are never asserted between type-expressions involving different outermost type-symbols.
In Section 8.4 we repeat the discussion in Section 7.6 about whether the notion of a class of displays in a category is a structure or a property: again this dispute is resolved by means of the distinction between strong and weak equivalences of categories.