When we introduced categories in Chapter IV we saw how they capture both semantic things such as topological spaces, and also the syntactic category of contexts and substitutions. The latter has chosen products, function-types etc simply because these have symbolic names, with rules which say just this. In order to give specific values to the interpretation functor [[-]]:Cn[]L® S, we therefore have to choose products and function-spaces in any category S in which we want to define semantics. On the other hand, mathematical intuition is that there is no God-given choice of the product of two topological spaces: these objects may always be interchanged with isomorphic copies.
Consequently there are strong and conflicting opinions about whether, when we say that a category has products etc , we mean them to be chosen or merely to exist. The second point of view is important even in formal reasoning, as a systematic way of discarding type-theoretic detail, cf Example 2.4.8. This conflict, to which we have referred in Sections 1.2, 4.5 and 7.1, is the price we have to pay for the versatility of category theory, but now we intend to resolve it, showing that it amounts to the difference between strong and weak equivalences .
Logicians, when they have considered semantics at all, have traditionally called it complete if there are enough models in a fixed universe of sets to distinguish the syntax (Remark 1.6.13). That is, if L\vDash f, ie some property f holds for all models of a theory L, then it is provable ( L\vdashf). We have already achieved this goal (for the fragments of logic we have discussed) by opening out the universe to encompass models built from the syntax itself. Now we want to go further, and treat syntax and semantics as equals - literally - requiring completeness of the syntax for the semantics as well as vice versa .
We aim to construct a language L from any suitable given category C, such that C @ Cn[]L. Theorem 4.2.12 did this for the unary case, where the structure [] just consisted of identities and compositions: the canonical elementary language L = L(C) has a type \qq X for each object of C and an operation-symbol \qq a for each C-morphism. L also names as laws all of the equations which hold in C, so \qqdash preserves the structure [], ie it is a functor, and \CloneL º C by Theorem 6.2.8(c).
Recall that we also called L an elementary sketch. Although we shall describe the language for products etc symbolically, many of the ideas of this section come from sketch theory (and others from sheaves).
Encoding operations We shall consider those connectives [] of type theory which are characterised by universal properties: products, sums, exponentials, quantifiers, List(-) and P(-), but not tensor products.
REMARK 7.6.1 Suppose that the objects X and Y have a product P and a sum S in a category C. This means that there are C-maps
|
|
|
\qq p0(pair(x,y))\leadsto x \qq p1( pair(x,y))\leadsto y
and an h-rule pair(\qq p0(z),\qq p1(z)) = z, which force pair to be the inverse of \qq p0,\qq p1. The definable operation for the sum goes in the opposite direction, so the encoding operation is
|
omitted diagram environment
for the encoding operation, in the ``product'' direction.
REMARK 7.6.2 P need not be the chosen product. Let a:Q º P be a semantic isomorphism, so we have another product diagram in C ( cf Theorem 4.5.6), and the composite \qq ao\pairX,Y,P obeys the laws for \pairX,Y,Q. Since inverses are unique, if this operation had also been named it would be provably equal to the derived form. For a semantically given category, therefore, it is harmless to name all of the diagrams (or as many as we please) which satisfy the universal property.
On the other hand, some diagrams may be products ``accidentally,'' not because we intended them to be. If we omit the corresponding pair encoding, we get a new product (that is, the syntactic product will not be isomorphic to the unwanted semantic one). Including its encoding operation in the language is how we give our approval to a particular semantic product, and this will ensure that the functor \qqdash preserves it.
EXAMPLE 7.6.3 The theory of monoids was given in Example 4.6.3(f) by a finite product sketch. A traditional syntactic account would say that multiplication has two (separate) arguments, but in this section all operations are treated as unary. We introduce a new object M(2) to be the source, and have to give additional information to force M(2) to be MxM. This is what the upper parts of the diagrams in Example 4.6.3(f) say. An interpretation of this finite product sketch in any category S with finite products is an interpretation of the underlying elementary sketch for which M¬ M(2)® M becomes a product cone in S. We have just described the syntax which is needed to do the same thing.
EXAMPLE 7.6.4 The canonical elementary language of a poset (S, £ ) lists the elements of S and all instances of the order relation £ between them; a general language L of this kind is simply a set S with any binary relation < , and \CloneL is the reflexive- transitive closure (Section 3.8).
Analogously to Cn×L we have the classifying semilattice Cn\landL of a Horn theory (S,\triangleright ) constructed in Theorem 3.9.1. By Proposition 3.9.3, any meet-semilattice arises in this way, where, if we want to specify that p = xÙy, we must add this fact to the language L, by writing
|
Canonical language The tradition of sketches is a minimalist one: to include only enough objects to determine the theory. We also want to show that categories which have all finite products, specified or not, arise as classifying categories. To deal with each of these applications, we give three versions of the definition.
The equational laws ought be treated in the same way as the additional structure such as products and function-types. However, it is technically simpler to assume in part (a) below that the unary part of the structure, which includes all of the equational laws amongst expressions, has been dealt with already (we did this in Theorem 3.9.7 for the lattice case too). The underlying elementary sketch is therefore a category.
To this we add encoding operations such as pair, split and (for function-types) \abs , together with the b- and h-rules that force them to be inverse to the corresponding definable operation in Remark 7.6.1.
DEFINITION 7.6.5 A language L for a small category C is
In the last case the interpretation [[-]] of L in S is defined, by Remarks 4.6.5, 4.7.4 and 5.5.2. Besides the operations and meta-operations of [], it must define the elementary language ( ie the objects, maps and composites) of C , and the encoding operations. These must be
|
The quoting operation \qqdash preserves just that structure of C which L names. In particular it is a functor because the identities and composites \qq a;\qq b = \qq a;b are named as laws of L.
REMARK 7.6.6 Let X¬ P® Y be any cone in C.
PROPOSITION 7.6.7 The role of categorical equivalence.
PROOF: Let P = FXxDFY.
omitted diagram environment
However, the unit h is also needed - and it must be natural - to show that U P = XxCY. []
DEFINITION 7.6.8 The structure [] is said to be conservative if, for any category C and subcanonical []-language L, the functor
|
Conservativity is a theorem that we must prove for each fragment [] of structure, along with giving its interpretation. Traditionally, this term means the relative property of the extension of a theory by some new connective, for example adding function-types to algebra. According to our definition, [] is conservative if the extension to the full []-structure is conservative relative to every intermediate structure L.
THEOREM 7.6.9 Let [] be a conservative structure, C a small category which has this structure and L a subcanonical []-language for C .
| |||||||||||||