Practical Foundations of Mathematics

Paul Taylor

9.1  The Predicate Convention

This section, which is an extended introduction to the chapter, sets up certain conventions for the way in which we shall use the familiar notation of the predicate calculus to explain a much more general and abstract theory. This overview is closer than is the rest of the chapter to Bill Lawvere's treatment of the semantics and Per Martin-Löf's of the syntax of type theory. We shall also show how the quantifiers fit into the general recursive scheme for constructing and interpreting type theory.

Throughout the book we have stressed the formal analogy between types and propositions. The only distinction between them in Chapter VIII, which set up the algebraic formalism for dependent types and its relationship with category theory, was the rather superficial one that proofs of propositions are not distinguished, so their displays are mono.

REMARK 9.1.1 The theme of this chapter is not the extensional difference between all maps and monos, but the separate roles which sets and propositions play in the quantifiers, comprehension and powerset.

(a)

Elements (terms) of the same set (type) are distinguished, but proofs are anonymous. (In Section 2.4 we mentioned the possibility that, by adding proof-terms, one might extract programs from proofs.)

(b)

Predicates f[x] depend on set-variables but not vice versa , so we may rearrange any context to put the set-variables first and the propositions dependent on them afterwards. This is an important technical simplification, which we shall exploit in Section  9.2.

(c)

Some forms of quantification, Sx:X.Y[x], $x:X.f[x], Px:X.Y[x] and "x:X.f[x], are allowed (Sections 9.3 and 9.4), but not others such as $y:f.X[y], because of (b),

(c)

and we may extract a witness x:X from a term of type Sx:X.Y[x] but, by (a), not from the provability of $x:X.f [x].

(d)

We may form the comprehension {x:X|f[x]} of a predicate on a set, giving a (sub)set, and

(e)

there is a set W whose elements name propositions (Section  9.5).

(f)

There may even be a type of all types - if for ``type'' we allow a domain with fixed points instead of a set with equality (Section 9.6) - but there is no proposition of propositions or proposition of sets.

We say that sets and propositions are types of two kinds (some authors say sort or order). These differences and the generality of which they are examples are sometimes presented in an extremely abstract way. Henk Barendregt uses *, [] and like symbols for kinds in describing his pure type systems [Bar92]. We end up proposing the use of such a formalism for semantic reasons, but we will keep the familiar terminology of the predicate calculus for the sake of motivation.

CONVENTION 9.1.2 However, we employ the words ``proposition'' and ``type'' as variables. In each section, these kinds are only required to obey the conditions of that particular section. They may in fact stand for the same kind - f may be a type like X - but we use this predicate convention to show where they are potentially different. What we say in propositional notation applies mutatis mutandis to types - in fact simply by transliteration of X for f etc .

Like characters in a Greek tragedy, prop, type, * and [] act out dramas about the essential interactions of things, in which their own identity is not relevant. In particular, the principle (a) of proof-anonymity is only used at one point in this chapter, namely in the discussion of the h-rule for the powerset (Remark  9.5.6). Assuming proof-anonymity would in fact make the second half of Section 9.4 pointless.

Classes of display maps   Chapter VIII set up the interpretation of types in context ( G\vdash X type) as pullback-stable ``display maps'' X® G. The partition of the class of all types into various kinds is handled by equipping the category with two or more classes of displays.

NOTATION 9.1.3 Following the predicate convention, we shall write

([G,x:X]® ^{[^(x)]}G) Î D     and     ([G,f]\hookrightarrow G) Î M

for sets and propositions respectively. But this is only a convention:

\hookrightarrow does not necessarily signify an injective function,

because this would mean that proofs were anonymous, which, as we have said, we shall usually not assume. There are, for example, realisability models of the predicate calculus in which proofs are distinguished and displays for propositions are not monos.

Note that nothing that we did in Chapter VIII mixes up the two classes, since there we considered displays one at a time. This unary closure condition gave rise to the []-modality ``stably'' in Example  8.3.6(k). It is the union of the kinds to which Theorem 8.4.10 refers.

The same semantic display map may belong to several classes, and be used as the interpretation of types of different kinds. In particular, we shall set out the theory of the existential quantifier and the type of propositions in detail, and deduce that of the dependent sum and type of types from it by substituting M = D and prop = type. Proof-anonymity is itself the parameter which distinguishes $ from S as we understand them semantically, so of course we are careful not to assume it.

Fibrations   We shall continue to work in the category of contexts and substitutions developed in the previous chapter, but now these contexts consist of types and propositions.

REMARK 9.1.4 Do not confuse [x:X,y:f[x]] with {x:X|f[x]} , which is the subset formed by comprehension. Compare the ``virtual objects'' consisting of program-variables and midconditions introduced in Remark  5.3.3: semantically, a context is not just a set but a subset of a particular ``ambient'' set. The semantics of the category of contexts is not Set but the comma category M¯ Set (Definition  7.3.8).

Until Section 9.5, where we consider comprehension as a type-forming operation, this means that the essential logical information is in a sense duplicated in the category. Exercise 9.9 explains how the results in Section 9.3 about factorisation systems in M¯ S relate to S itself.

omitted diagram environment

REMARK 9.1.5 Cn^×_type, which consists of set-only contexts, is called the base category. For each set (or each context G consisting only of sets), there is a subcategory of this big category that consists of the predicates f[[(x)\vec]] over G; it is called the fibre P(G). For each function u:G®D, there is a substitution or inverse image functor u^*:P(D)® P(G); the assignment u® u^* provides a functor P(-):(Cn^×_type)^op® Cat, which is known as an indexed category. The big category Cn^×_type|prop whose contexts consist of both types and propositions collects all of these fibres together. There's a proposition-erasing functor P:Cn^×_type|prop® Cn^×_type, called a fibration. Beware that P and P are in different typefaces!

Bill Lawvere and Jean Bénabou used fibrations to study the quantifiers and infinitary limits and colimits. We show in Section 9.2 that fibrations capture the independence of types from propositions (Remark 9.1.1(b)), but this is not relevant to the quantifiers (it is to comprehension).

The quantifier formation rules   As for the predicate and l-calculi (Sections 1.5 and 2.3), we present the syntactic rules for the quantifiers in both the box and sequent styles.

REMARK 9.1.6 The quantifier formation rule binds a variable, so the box begins with a context-formation (Definition 8.2.2).

The indirect ("Á )- and ($E )-rules define terms

lx.p       and       let(x,y)bec inf

which bind the variables x and y, so they are subject to a- equivalence, as are the type formation rules. Corresponding to the formation rules, there are also type and term equality rules, such as

As in Section 1.6, types and terms may be imported into boxes from above, and exported if wrapped in the quantifier or indirect operation.

Adjointness in foundations   These are symbolic trivia: what we really want to know is how the indirect, b- and h-rules correspond to the universal properties of ve and ev.

REMARK 9.1.7 Bill Lawvere finally brought symbolic logic into the heart of mathematics by recognising the bijective correspondences

REMARK 9.1.8 Since universal properties describe objects in category theory only up to isomorphism, we shall understand notation such as $x.f in the same way: it means any object y which satisfies the introduction, elimination, b- and h-rules for an existential quantifier for the predicate f[x] over the type X. This need not be the string ``$x.f,'' just as X® Y in Section  4.7 did not have to be literally an arrow. In fact the symbolic rules also characterise y only up to isomorphism.

Following the preference stated in Chapter VII, we shall discuss the universal properties of the quantifiers diagrammatically, instead of using Lawvere's adjunctions.

Substitution and the Beck-Chevalley condition   We are used to substituting directly under the quantifiers: Definition  1.1.10(d) said that u^*$x:X.f is equal to $x:u^*X.u^*f. We don't state such a rule here because to assert equalities between types may conflict with their possibly different histories of formation.

REMARK 9.1.9 Instead of asserting a substitution rule directly for the types, we give stronger indirect rules for the terms. Then, as for all universal properties, we prove that u^*Qx:X.f º Qx:u^*X.u^*f, in a unique way which commutes with the structure.

Categorically, the contexts involved form a pullback as shown on the left,

omitted diagram environment

and we want the diagram on the right to commute, in the sense that a certain natural transformation (provided by the universal properties of Qx_G and Qx_D ) is invertible. This equation between types is known as the Beck-Chevalley condition, although it was Lawvere and Bénabou who identified it in categorical logic, respectively attributing it to Jon Beck and Claude Chevalley because of analogous properties in their work in the descent theory of algebraic geometry.

This property is often presented as an additional burden: something extra to be checked after the already heavy labour of the construction of the concrete objects to be used in the interpretation. Of course, if you choose to define the quantifiers categorically as the adjoints to substitution, then this condition does need verification. But we give another characterisation of " with the condition built in, so it can do the work for us: we choose the values of quantifiers of the form "x:X.f where X and f are type- and proposition- symbols, and then the substituted forms "x:u^*X.\nearrow ^*f are derived from the Beck-Chevalley condition.

The recursive definition of interpretations   Theorem 8.4.4 showed how to use the history of formation of types and terms to interpret generalised algebraic theories in categories with display maps.

REMARK 9.1.10 The quantifiers and their terms contribute new cases to this structural recursion, just as the simply typed l-calculus in Remark 4.7.4 extended the interpretation of algebra in categories with products. By the recursion hypothesis, we already have

REMARK 9.1.11 For the sake of making [[-]] into a bona fide functor, let us consider briefly how to choose a particular object from the isomorphism class which the universal property provides. In Zermelo type theory (Remark 2.2.4) this may be done by fiat for $, as comprehension names canonical subsets for the image factorisation.

The formal rules as we give them say that the Beck-Chevalley condition only holds up to unique isomorphism, even in the syntax. Without some trick, $x:X.f must be regarded as a new proposition- symbol, even when X and f are type- expressions: f^*$x:X.f is a substitution-instance of it, but $x:f^*X.f^*f is not.

We would like to find some way of prescribing interpretations to make the Beck-Chevalley condition hold up to equality. Although we have introduced it semantically, this is really a symbolic problem: does cut or substitution commute with the type formation rules? If it does then once again we need only choose the results of quantification at type- symbols. Recall that Theorem 8.4.4 did this for unquantified type-expressions: given a choice of semantic displays at type-symbols, it used pullbacks anchored there to interpret type-expressions.

Since f^*\propext (\nearrow ^*f) = (f;\nearrow )^*\propext f, there is no difficulty with comprehension (or the powerset). In the cases of $ and ", substitutions may be embedded in two places: for the range and the body. Corollary  9.4.15 shows that