Algebra with Dependent Types

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*® (*ob**C*)^{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
\coprod_{x} *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*] = *T*^{n}(*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
*tgt***f** = *src***g** *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.