McLarty: Elementary Categories, Elementary Toposes

Javascript Interactive Higher-Order Theorem Prover

Automated Reasoning in Higher Order Logic

This page was created and is maintained by Chad E Brown.

Colin McLarty. Elementary Categories, Elementary Toposes. Oxford University Press, 1992. (Available via Amazon)

Chapter 1: Rudimentary structures in a category. McLarty begins by giving the axioms for a category and the definitions of isomorphisms, monics, epics, terminal, initial and zero objects. He then introduces generalized elements, including the special cases of global elements (terminal domain) and the generic element (identity arrow). Two arrows are equal iff they agree on all generalized elements (consider the generic element!). An arrow is monic iff it is one-to-one on generalized elements. An arrow which is onto on generalized elements is split epic (has a right inverse, stronger than epic). An arrow is an iso iff it is one-to-one and onto on generalized elements.

Chapter 2: Products, equalizers, and their duals. After introducing the notion of a commutative diagram, McLarty defines product diagrams using the usual universal mapping property. Any object isomorphic to a product object can be made into a product diagram by composing the projections with the isomorphism. Conversely, the objects of any two product diagrams are isomorphic via the universal maps (and the isomorphism respects the projections). All generalized elements of a product object AxB are of the form <x,y> where x and y are generalized elements of A and B (resp.) with the same domain. Since product arrows satisfy (hxk) o <f,g> = <hof,kog>, we also have the identity (hxk)(<x,y>) = <h(x),k(y)> in terms of generalized elements of the (product object) domain of hxk. 1xA is always isomorphic to A by the unitary isomorphism <!,1_A> for A (with inverse given by the projection 1xA->A). These arrows are natural ("get along with arrows") so they define natural isomorphisms (each the inverse of the other) between the functor F:C->C given by F(A) = 1xA and F(f) = 1_1 x f and the identity functor on C (here, F depends on the selection of the product diagrams) Similarly we can define a "twist" for each AxB and BxA, which gives a natural isomorphism between functors F(A,B) = AxB and G(A,B) = BxA under the appropriate existence assumptions.

The definition of (binary) product diagrams can be generalized to a product diagram for any finite number of objects. For zero objects, a product diagram is simply a terminal object. Every object (with identity) is a product diagram for itself (so that we have such products of a single object in every category). If we have binary products, then we have products for any finite number of objects greater than two (by taking AxBxC as (AxB)xC and composing projections). As above, we can obtain natural isomorphisms (called "associativity arrows") between AxBxC, (AxB)xC, and Ax(BxC).

Coproducts diagrams are the dual of product diagrams. Note that the description in terms of generalized elements fails. Next, we have equalizers and coequalizers. Every equalizer is monic.

Chapter 3: Groups. In any category C with all finite products, we can define a group to be an object G and arrows e:1->G, i:G->G, m:GxG->G where the appropriate diagrams (corresponding to the axioms of group theory) commute. A group homomorphism is an arrow from the object of one group to the object of another which agrees with the arrows of the groups. (Note that every such category C has at least one group, given by a terminal object.) Since such homomorphisms compose, we have the category Grp_C of all groups in C. (The group given by a terminal object of C is a zero object in Grp_C.) We can do this for any algebraic structure which is given purely by operators and equations (e.g., abelian groups, rings, commutative rings). We cannot do this for fields since we have no way of saying something like "x not 0 implies i(x) is x inverse." (We only have equations, no logic.)

Chapter 4: Sub-objects, pullbacks, and limits. We can consider a monic as a subobject of its codomain (or, as is sometimes done, take a subobject to be an equivalence class of monics). In terms of generalized elements, we say x:A->C is a member of i:B>->C if x factors through i. Given monics i:A>->C and j:B>->C, we say i <= j if i factors through j (so, in terms of generalized elements, i is a member of j). In such a case, i must factor through j via a monic, giving a subobject of B. We can say i and j are equivalent subobjects (equal if we take this equivalence class of monics to be the definition of subobjects) if they each factor through each other. In such a case, they must factor through each other by isos which are mutually inverse. In terms of generalized elements, two subobjects are equivalent if they contain the same members. Equalizers of f and g characterize the subobject containing precisely the generalized elements x so that f(x) = g(x).

Pullbacks can be characterized as a (binary) product followed by an equalizer. A pullback of a monic is monic (giving "preimages" in terms of generalized elements). A pullback of two monics gives an intersection subobject (which acts as "intersection" in terms of generalized elements). We have the pullback lemma and consequences.

Products, equalizers and pullbacks are all special cases of limits of diagrams. A limit is a terminal object in the category of cones over a given diagram. We have the dual notions of cocones and colimits and the special cases of coproducts, coequalizers and pushouts. Assuming certain products exist, we can construct limits by forming the product of all objects involved in the diagram and the product of all codomain objects involved in the diagram indexed over the arrows in the diagram. Then we form two arrows from the first product to the second in such a way that the equalizer of these two arrows, when composed with the projections of the first product, gives the limit of the diagram.

A category with a terminal object, binary products, and equalizers has all finite limits. Also, a category with a terminal object and pullbacks has all finite limits.

Chapter 5: Relations. A relation from A to B is a subobject of AxB. Such a subobject is given by a monic arrow <h,k>:C>->AxB. When such an arrow <h,k> is monic, we say h and k are jointly monic. Note that if either h or k is monic, then <h,k> is monic. The projection arrows p1:AxB->A and p2:AxB->B provide an example of arrows so that <p1,p2> is monic, but neither p1 nor p2 are (in general) monic. One example of a relation is given by the diagonal delta = <1,1>:A>->AxA. In terms of generalized elements we have <x,y> in delta iff x = y. Given any relation, we can form the converse relation by composing with the twist arrow.

A relation is reflexive if it contains delta. A relation is symmetric if it contains its converse. Both reflexivity and symmetry can be characterized (in the usual way) using generalized elements. A relation r is transitive if for every <x,y> and <y,z> (generalized elements) in r, we have <x,z> is in r. Transitivity can also be characterized by diagrams.

Another example of a relation is that of a kernel pair. Given any arrow f:A->B, we can form the pullback of f along itself to obtain arrows h,k:C->A. <h,k>:C>->AxA is monic by the uniqueness condition of the UMP of pullbacks. <h,k> gives the equivalence relation on A characterized by the condition: <x,y> is in <h,k> iff f(x) = f(y). An equivalence relation is called effective if it can be represented as the kernel pair of some f.

Chapter 6: Cartesian closed categories. We define exponents (in a category with finite products) by the universal mapping property. A category with finite products and exponents is a Cartesion Closed Category (CCC). In such a category, every arrow f:TxA->B has a unique transpose _f:T->B^A; we also call f the transpose of _f. Note that ev o _f x 1_A = f (so we have a formula for the transpose in one direction). We can define a functor ^A:C->C by taking B to B^A and f:B->B' to f^A = _(f o ev). (Note that _ev = 1_(B^A) since ev o 1_(B^A) x 1_A = ev.) We can prove this functor preserves composition by using the standard technique of checking that the transposes of both sides of an alleged equation are equal (in this case, we check that g^A o f^A has the property which uniquely determines the transpose of g o f o ev).

We can further internalize composition by defining c to be the transpose of ev o 1xev o assoc (Idea: <<f,g>,x> |-> <f,<g,x>> |-> <f,g(x)> |-> f(g(x)).) Then, for any r:TxA->B and s:TxB->C ("T-indexed families of arrows") we have c o <_s,_r> = _(s o <pi_1,r>) ["T-indexed composition"]. We can see this (with a little work!) by considering the transpose of both sides. This determines how c behaves on generalized elements, and can be used to show that c (actually, here we are talking about several c's, depending on the choices of A, B and C) is "associative." The idea is to show c(<_t,c(<_s,_r>)) = c(<c(<_t,_s>),_r>) [again, these are all different c's in general]. By taking the transpose, we have to show t o <pi_1, s o <pi_1,r>> = t o <pi_1,s> o <pi_1,r>. But this is easy.

If a CCC has an initial object 0, then every Ax0 (and 0xA) is initial (since Ax0->B corresponds to 0->B^A), and every B^0 is terminal (since A->B^0 corresponds to Ax0->B). If there is an arrow f:A->0, then A is initial (consider the graph of f, Gamma(f):A>->Ax0 which must be iso since it is monic and split epic since Ax0 is initial). In any category, an initial object is called strict if the only objects with arrows into it are initial. So, in any CCC, initial objects are strict. In particular, the only CCC with an arrow 1->0 is the degenerate CCC in which all objects are isomorphic zero objects. For a CCC C, the functor -xA:C->C (i.e., "product with A") preserves initial objects, coproducts, coequalizers and pushouts [it preserves all colimits since it is left adjoint to -^A].

Chapter 7: Product operators and others. We can expand the language of category theory to include operators -x-, p1--, and p2-- to pick out particular product diagrams for each two objects. Similarly, we can expand the language to include a constant for the terminal object and operators to pick out equalizers. This allows us to talk about a specific product/terminal object/equalizer without having to say "up to isomorphism" all the time. The UMP of each of these limits can be stated as "forall exists unique" statements. If we like, we can expand the language further to give functions corresponding to these statements (semantically, this expansion is of less consequence since such functions are already uniquely determined). For example, for the terminal object we can include a function !-.

Chapter 8: Functors and categories. A functor from a category A to a category B maps A-objects to B-objects and A-arrows to B-arrows preserving domains, codomains, identities, and composition. A functor F is faithful if for each objects A', A'' F gives a one-to-one map from Hom(A',A'') to Hom(F(A'),F(A'')); such an F is full if for each objects A', A'' F gives an onto map from Hom(A',A'') to Hom(F(A'),F(A'')). In general, F may or may not preserve certain limits. Even if F does preserve, for example, products, there is no guarantee that F will take selected products to selected products. We may consider CAT to be the category of "all" categories with functors between them.

We can construct new categories from given categories. For example, we can easily construct the product category AxB from categories A and B. This, with the projection functors, gives a product diagram in CAT. A subcategory of A is a monic i:S>->A. This may be the inclusion functor if S actually consists of objects and arrows from A. If i is full, then we have a full subcategory. Given two functors with domain category A and codomain category B, we can form the subcategory of A on which they agree and this subcategory gives the equalizer of the functors. So, CAT has all finite limits (the category 1 is terminal). Given a category A, we can form the arrow category A^2 (this may also be interpreted as the category of all functors from the category 2 to A with natural transformations as arrows). Given an object B of A, we can form the slice category A/B of arrows in A with codomain B and commutative triangles. We noted in Chapter 3 that we can form Grp_A. Also, every category A has an opposite category A^op in which we reverse all the arrows. We sometimes say that a functor G:A^op->B is a contravariant functor from A to B.

-xB:A->A (if A has binary products; always preserves equalizers and pullbacks; preserves all colimits if A is a CCC; does not preserve terminals)

-^B:A->A (if A is a CCC; preserves terminal, products, equalizers and pullbacks)

B*:A->A/B (if A has products; takes C to p1:BxC->B; note: Sigma_B o B* = Bx-:A->A)

The terminal category in CAT is 1 (one object; identity arrow). Another finite category is 2 (which looks like alpha:0->1). Functors 1->A correspond to the objects of A. Functors 2->A correspond to the arrows of A. As a result, in terms of generalized elements, any two functors F,G:A->B are the same iff they agree on 2-elements (generalized elements of A with domain 2). We call an object with this property a "generator", so 2 is a generator of CAT. Note that we may have different such functors F and G which agree on global elements. For example, consider any category Grp_A and the functor which is the identity on objects but takes all arrows to the zero homomorphism. Such a functor agrees with the identity functor on objects, but is clearly different for nontrivial Grp_A.

Chapter 9: Natural transformations. CAT is actually Cartesian closed. We construct B^A to be the functor category with objects functors from A to B and arrows natural transformations between such functors. A natural transformation from F:A->B to G:A->B is a family of B-arrows eta_A':F(A')->G(A') indexed by A-objects A' satisfying G(f) o eta_dom(f) = eta_cod(f) o F(f). (We can equivalently describe a natural transformation as a functor eta:A->B^2 so that D o eta = F and C o eta = G.) A natural transformation is a natural isomorphism if each component is an isomorphism arrow. Natural transformations compose componentwise. So, we can make the category B^A. Also, we have the functor ev:B^A x A -> B given by ev(F,A') = F(A') and ev(eta,f) = ev(eta,1_cod(f)) o ev(1_dom(eta),f) = eta_cod(f) o dom(eta)(f) [= cod(eta)(f) o eta_dom(f)]. We prove ev is really a functor using the bifunctor theorem, which roughly says, that an alleged functor F:AxB->C is a functor if it is a functor in each of its arguments and satisfies the "interchange law" F(f,1_cod(g)) o F(1_dom(f),g) = F(1_cod(f),g) o F(f,1_dom(g)). (ev satisfies the interchange law by the definition of naturality.) Finally, we can construct the transpose of F:TxA->B by Currying and check that this is really the transpose.

In more detail, the bifunctor theorem states the following: Suppose we have families of functors L_A':B->C and R_B':A->C (indexed by objects A' of A and B' of B) such that L_A'(B') = R_B'(A') for every A' and B'. Suppose further that the families satisfy the "interchange law" R_B''(f) o L_A'(g) = L_A''(g) o R_B'(f) for every f:A'->A'' and g:B'->B''. Then there is a unique functor F:AxB->C such that F(A',-) = L_A' and F(-,B') = R_B' for every A' and B'.

An equivalence situation consists of two functors F:X->A and G:A->X and natural isomorphisms phi:1_X->GF and psi:1_A->FG. In such a situation, F and G must both be full and faithful. Also, whenever we have a full and faithful functor F:X->A so that every object B is isomorphic to some FY, then we call F an equivalence functor. Assuming some form of the axiom of choice, we can find a G:A->X and natural isomorphisms phi and psi giving an equivalence situation.

Here are some interesting facts about natural transformations. (See Exercises 9.4 and 9.7.) Suppose G,H:X->A, and eta:G->H. Then, for any F:A->B, F(eta):FG->FH where F(eta)_X' = F(eta_X'). Also, for any F:Y->X, eta_F:GF->HF where (eta_F)_Y' = eta_{FY'}. We might write F(eta) as F^2 o eta (thinking of eta:X->A^2). We might also write eta_F as eta o F. Composition by F:A->B in this way gives a functor F^X from A^X to B^X. Precomposition by F:Y->X in this way gives a functor A^F from A^X to A^Y. So, all this reduces to describing the functors -^X:CAT->CAT and A^-:CAT^op->CAT.

Chapter 10: Adjunctions. Given a functor F:X->A and object A' of A, a universal arrow from F to A' is an X-object X' and A-arrow epsilon:FX'->A' so that for every A-arrow f:FY->A' there is a unique X-arrow g:Y->X' so that f = epsilon o Fg. Universal arrows are unique up to a unique commuting isomorphism. We can also define the dual notion of a universal arrow from A' to F.

An adjunction consists of two functors F:X->A and G:A->X and natural transformations eta:1_X->GF and epsilon:FG->1_A satisfying the triangular identities epsilon_FX' o Feta_X' = 1_FX' and Gepsilon_A' o eta_GA' = 1_GA'. (Reading these identities at a higher level of abstraction, we have the natural transformation F->FGF->F given by epsilon_F o F(eta) is 1_F and the natural transformation G->GFG->G given by G(epsilon) o eta_G is 1_G.) We say F is left adjoint to G (or, F -| G) and call eta the unit and epsilon the counit of the adjunction. Adjoints are unique up to a unique commuting isomorphism, as usual. Each eta_X' gives a universal arrow from X' to G and each epsilon_A' gives a universal arrow from F to A'. The adjunct of an A-arrow f:FX'->A' is given by Gf o eta_X'. The adjunct of an X-arrow g:X'->GA' is given by epsilon_A' o Fg. In order to obtain an adjunction, it is enough to have a functor F:X->A and objects (which we will call) GA' with universal arrows epsilon_A':FGA'->A' from F to A'. In such a situation, there is a unique functor G taking objects A' to GA' and epsilon is a natural transformation from FG to 1_A. We can also specify an adjunction by giving a functor G:A->X and universal arrows eta_X':X'->GFX' (with objects FX') from X' to G.

We can also characterize adjunctions as isomorphisms between comma categories which commute with base functors. The comma categories in question are (F,A) [objects are pairs <X',f:FX'->A'> and arrows are pairs <h:X'->X'',k:A'->A''> which make the appropriate square commute] and (X,G) [objects <g:X'->GA',A'> and arrows <h:X'->X'',k:A'->A''>]. We have base functors b:(F,A)->XxA and b:(X,G)->XxA. Given an adjunction, we can define an isomorphism I:(F,A)->(X,G) taking f:FX'->A' to its adjunct g:X'->GA'. This isomorphism commutes with the base functors. Conversely, given an isomorphism I:(F,A)->(X,G) which commutes with the base functors we have a correspondence between arrows f:FX'->A' and g:X'->GA'. We can build an adjunction by defining eta_X' = I(X',1_FX') and epsilon_A' = I^{-1}(1_GA',A').

Finally, we can compose adjunctions F-|G and F'-|G' to obtain FF' -| G'G. For example, suppose we have a topological space X with O=O(X) the set of open sets, K=K(X) the set of closed sets, and P=P(X) the power set of X. We have obvious functors int:P->O, cl:P->K, and inclusion functors i:O>->P and j:K>->P. It is easy to check that i -| int and cl -| j. Composing these adjunctions we have cl o i:O->K is left adjoint to int o j:K->O (closure is left adjoint to interior).

Colimits -| Constant -| Limits (special case: Coproducts -| Diagonal -| Products)

A very useful result is that right adjoints preserves limits (RAPL) and left adjoints preserve colimits. [Note that -xA cannot, in general, have a left adjoint since it does not preserve terminals.]

Chapter 11: Slice categories. We can think of an arrow f:A->B as a B-indexed family of objects. If B is 1 then arrows f:A->1 correspond precisely to objects A (so, for every category C with terminal 1 we have C is isomorphic to C/1). If a category C has all finite limits, then so does each slice C/A. Products in C/A are constructed using pullbacks in C. Equalizers in C/A are constructed using equalizers in C. So, Sigma_A:C/A->C preserves equalizers, but not products or terminal objects (in general). Sigma_B -| B* (the correspondence is given by k:Sigma_B(g)->A is adjoint to <g,k>:g->B*A). As a result, Sigma_B preserves all colimits.

In a CCC C with all finite limits, we can construct a right adjoint Pi_B to B* by forming the pullback of f^B:A^B->B^B and the name of 1_B:B->B ('1_B':1->B^B--note this is monic). This gives Pi_B(f) (taking an object of C/B to an object of C) and a monic arrow i:Pi_B(f)>->A^B. On arrows, Pi_B takes k:f->g (where f:A->B and g:D->B) to the pullback of the triangle consisting of k^B:A^B->D^B, f^B and g^B along the pullbacks defining Pi_B(f) and Pi_B(g). A theorem on pullbacks allows us to "pull back" such diagrams.

In fact, we have that a category C with all finite limits is CCC if each B* has a right adjoint. This follows from the fact that each functor -xB factors as Sigma_B o B* which has right adjoint Pi_B o B*.

Each slice Set/B can be considered the category of bundles over B. Sigma_B takes the bundle given by f:A->B to the set A (it pastes the bundles back together). B* takes a set A and makes B many copies of it. Pi_B takes the bundle given by f:A->B and returns the set of all g:B->A so that fg=1_B. Note that this is equivalent to the product set Pi_{b in B}(f^{-1}(b)) (product of the bundles).

A category C may be CCC and yet have slices C/A which are not CCC. We do have that if A^B is an exponential of A by B in C, then for each object D, D*(A^B) is an exponential of D*A by D*B in C/D.

Up to isomorphism, the slice of a slice (A/B)/f is a slice A/C (where f:C->B). In fact, Sigma_f:(A/B)/f->(A/B) agrees, via this isomorphism, with Sigma_f:(A/C)->(A/B) given by Sigma_f(g:D->C) = f o g and taking the arrows to themselves (considered as arrows of the other slice). So, this "composition" functor Sigma_f is, up to isomorphism, a slice functor, and thus has a right adjoint f*:(A/B)->(A/C). f*g is given by the pullback of g along f.

A category is locally Cartesian closed (LCCC) if all its slices are CCC's. If a category is LCCC, then so are all its slices. In an LCCC A, each f* has a right adjoint Pi_f. Also, f* preserves exponents in such a case.

We can describe the slice categories Set/I as bundles indexed by I. Since Set is a topos, Set/I is a topos (hence CCC), so Set is LCCC (as is any topos). Given f:I->J, we can describe the adjoint functors Sigma_f -| f* -| Pi_f in terms of bundles. Sigma_f:Set/I->Set/J takes bundles over I to bundles over J by unioning the germs at i with f(i)=j. f*:Set/J->Set/I takes bundles over J to bundles over I with each germ over i a copy of the germ over j with f(i)=j. Pi_f:Set/I->Set/J takes bundles over I to bundles over J by taking the product of the terms at i with f(i)=j.

Chapter 12: Mathematical foundations. McLarty describes two styles of mathematical foundations for general category theory. The first is a set-theoretic foundation. We may use GB set theory and distinguish between small and large categories, locally small categories (those with Hom-sets), and well-powered categories (those with sets of subobject representatives). The problem with this foundation is that we cannot construct certain large categories such as Set^Grp. A solution is to use Grothendieck universes. That is, we add an axiom to ZF that there is a set V which satisfies the ZF axioms (note that this must be stronger than ZF since it implies the consistency of ZF). Then we relativize the size concepts to V-small, V-locally small, and so on. Then, if we need to, we can add axioms asserting the existence of larger ZF universes V', V'', and so on. MacLane's axiom only asserts a single universe V. MacLane considers this sufficient for most purposes.

The second approach is to axiomatize the category of all categories (Lawvere's approach). Here, we start by asserting the existence of categories 1 (as the terminal category) and 2 (with two global elements) as well as products, equalizers, exponents, an initial category, coproducts, and coequalizers. In this setting, categorical structures are described by their generalized elements. There is no authoritative axiomatization.

Chapter 13: Basics. A topos is a CCC (all finite limits and exponents) with a subobject classifier. A subobject classifier is an object Omega and "truth" arrow t:1->Omega so that for every monic s:S>->A there is a unique "classifying arrow" Chi_s:A->Omega so that s is the pullback of t along Chi_s. It follows that equivalent subobjects have equal classifying arrows. Also (since t is monic), every arrow A->Omega corresponds to a subobject. So, we have Sub(A) is isomorphic to Hom(A,Omega). What does this mean in terms of functors? For a small topos E, we have the representable functor yOmega = Hom(-,Omega):E^op->Set and the functor Sub:E^op->Set which acts on arrows by pullbacks (i.e., f:A->B induces Sub(f):Sub(B)->Sub(A) by taking f*S>->A to be the pullback of S>->B along f). yOmega is naturally isomorphic to Sub via the above correspondence. This isomorphism is natural since Chi_s o f = Chi_{f*s} (see exercise 13.3). (Actually, Sub maps into the category of posets and we compose with the appropriate forgetful functor to get the functor above.)

So, what is the conclusion? Given a CCC, we have a subobject classifier iff the functor Sub is isomorphic to a representable functor in Set^{E^op}. To see the "if" direction, use Yoneda. That is, given a natural isomorphism eta:yOmega->Sub, the Yoneda Lemma says eta is determined by eta_Omega(1_Omega) in Sub(Omega). Let t:A>->Omega be (a monic representing) the subobject eta_Omega(1_Omega). At each object B and f:B->Omega, eta_B(f) = eta_B(1 o f) = eta_B(Hom(f,Omega)(1)) = Sub(f)(t). That is, eta_B(f) is the subobject of B given by the pullback of t along f. Since eta_B:Hom(B,Omega)->Sub(B) is an isomorphism (of sets), for every subobject i of B there is a unique f so that i = eta_B(f), i.e., i is the pullback of t along f. This is precisely the definition of subobject (except that we need to know A is terminal).

To see that A is terminal, consider the subobject 1_1:1>->1. There is a unique t':1->Omega so that 1_1 is the pullback of t along t'. Using the UMP of this pullback with 1:A->A and !:A->1, we obtain an isomorphism between A and 1.

Assume we are working in a topos. Every monic is an equalizer (of its characteristic arrow and t!). [Note in general we have pullbacks of global elements are equalizers.] Every monic epic is iso (since an epic can only possibly equalize two arrows which are already equal).

Note that in terms of generalized elements, we have Chi_s(x) = t! iff x is "in" s. Or, x is "in" s iff Chi_s(x) is "in" t (considered as a subobject of Omega).

Chi_{1_1} = t. Chi_{1_E} = t!:E->Omega. Chi_t = 1_Omega. Also, t! o f = t! for any f. (That is, if we write t_B = t!:B->Omega and we have f:A->B, then t_B o f = t_A.)

Conjunctions are given by the arrow and:Omega x Omega -> Omega which classifies the subobject <t,t>:1->Omega. We may abbreviate "and o <h,k>" by "h and k". "u and v" = t! iff u=t! and v=t!. For subobjects r and s, Chi_{r intersect s} = Chi_r and Chi_s (since r intersect s is the pullback of <t,t> along <Chi_r,Chi_s>). In terms of generalized elements, (Chi_s and Chi_r)(x)=t! iff Chi_s(x)=t! and Chi_r(x)=t!. We can show that conjunction is commutative, associative, and idempotent using intersections. Also, "u and t" = u.

[Note: intersection is a natural transformation from Sub x Sub to Sub. There is a corresponding natural transformation from yOmega x yOmega to yOmega. This corresponds to an arrow y(Omega x Omega)->yOmega. By the Yoneda Lemma, this corresponds to a member of Hom(Omega x Omega,Omega). That member is the arrow and:Omega x Omega -> Omega.]

Let <=1 be the equalizer of and,p1:Omega x Omega -> Omega. In terms of generalized elements, we can write u <=1 v whenever <u,v>:T->Omega x Omega factors through <=1. Then we have u <=1 v iff u = u and v. Properties of conjunction imply u <=1 t, <=1 is reflexive, transitive, and antisymmetric. Also, Chi_r <=1 Chi_s iff r is a subobject of s (i.e., r factors through s).

Since <=1 is an equalizer, it is monic. Let ->:Omega x Omega -> Omega be its classifying arrow (the "material implication" arrow) and write u -> v for -> o <u,v>. u->v = t! iff u <=1 v. This arrow -> induces an operation => on subobjects. For subobjects Q, R, and S, we have (S intersect Q) smaller than R iff S smaller than (Q => R). With S = Q=>R, this implies Q=>R is the largest subobject such that (Q=>R) intersect Q is a smaller than R.

[As above, =>:Sub x Sub -> Sub corresponds to -> in Hom(Omega x Omega,Omega) via the Yoneda Lemma.]

For every A, Omega^A is the power object of A with subobject eps_A>->A x Omega^A classified by ev o twist. We can abbreviate <x,h>:T->AxOmega^A "in" eps_A (as a generalized element) by x eps_A h. This is equivalent to saying ev o <h,x> = t!. For any global element x:1->A and arrow w:A->Omega, we have x eps_A 'w' (the name of w) iff w o x = t iff x eps w* (where Chi_{w*} = w--i.e., w* is w*t).

t_E = t!:E->Omega classifies the maximal subobject 1_E:E>->E. The name 't_E':1->Omega^E is monic and has a classifier Forall_E:Omega^E->Omega. Note that we can say for any f:A->Omega^E, Forall_E o f = t! iff f = 't_E' o !_A. (By using the pullback property and the fact that there is only one arrow !_A:A->1, we have an analogous result whenever the subobject we are classifying is a monic with terminal domain.) In terms of generalized elements, we have 't_E' o !_A is the only generalized element of 't_E' with domain A.

From any relation r:R>->BxA, we can form the subobject of B representing the universal quantification over A (really the projection) of r by taking the subobject (Forall a)r to be the pullback of 't!' along the transpose of Chi_r (i.e., _(Chi_r):B->Omega^A). This subobject is classified by Forall_A o _(Chi_r) (by the pullback lemma). For any subobject s:S>->B and relation r:R->BxA, we have s is smaller than (Forall a)r iff sxA is smaller than r. We can prove this by noting that _(Chi_r) o s = _(Chi_r o (sxA)), 't_A' = _(t_(1xA)), and 't_A' o !_S = _(t_(1xA) o !_S x A) = _(t_(SxA)). Putting this together with the comment above, we have Forall_A o _(Chi_r) o s = t! iff _(Chi_r) o s = 't_A' o !_S iff Chi_r o (sxA) = t_(SxA). That is, s is smaller than (Forall a)r iff sxA is smaller than r.

[Each f:A->B gives a functor f*:Sub(B)->Sub(A). In a topos, we have a right adjoint Forall_f:Sub(A)->Sub(B) of f* for each f:A->B. For a fixed f:A->B, we have a natural transformation with Z-component Forall_{fxZ}:Sub(AxZ)->Sub(BxZ). This corresponds to a natural transformation from Hom(Ax-,Omega) to Hom(Bx-,Omega), which in turn corresponds to a natural transformation from Hom(-,Omega^A) to Hom(-,Omega^B). By the Yoneda Lemma, this corresponds to an arrow in Hom(Omega^A,Omega^B). In the particular cases of !_A:A->1 (using 1xZ is isomorphic to Z for all Z--naturally in Z), we have a natural transformation Forall_{!_A x -}:Sub(Ax-)->Sub(-) which corresponds to an arrow Forall_A:Omega^A->Omega. This is the arrow defined above.]

Generalized elements of intersections behave nicely in that x is in q intersect r iff x is in q and x is in r.

For a relation r:R>->BxA and any w in B (w:S->B), we have w is in (Forall a)r iff wxA is in r (proven by considering _(Chi_r) o w = 't_A' o !_S iff _(Chi_r o wxA) = _(t_(SxA)) iff Chi_r o wxA = t!). This implies that such a w is in such a (Forall a)r iff for every <h,k>:C->SxA we have <w(h),k> is in r.

For two subobjects q:Q>->A and r:R>->A of A and the generalized element w:S->A of A, w is in q=>r iff w(w*q)) is in r. To prove this, we note that w(w*q) is in q (since the pullback square defining w*q commutes). If w(w*q) is in q=>r, then it is in (q=>r) intersect q, and hence in r. Conversely, assume w(w*q) is in r. Then w*q is smaller than w*r. So, Chi_q o w = Chi_{w*q} = Chi_{w*q intersect w*r} = Chi_{q intersect r} o w. This implies w factors through q=>r, which is the equalizer of Chi_q and Chi_{q intersect r}. So, we have the result. A corollary is that w is in q=>r iff for every h:C->S, with w(h) in q we have w(h) is in r.

Chapter 14: The internal language. The internal language of a topos E is a many-sorted language with a sort for each object. The terms are generated as follows: x:A where x is a variable of sort A, c:A where c:1->A in E, fs:B where f:A->B in E and s is a term of sort B, <s1,s2>:AxB where s1 is a term of sort A and s2 is a term of sort B, "lam y.s":B^A where y is a variable of sort A and s is a term of sort B.

For every term s:B of the internal language with free variables from the list _y = <y1:A1, . . ., yk:Ak>, we have the interpretation |s|_y:A1x...xAk->B of s. This is defined inductively on the construction of terms by taking |yi:A|_y to be the projection, |c|_y to be c!, |fs|_y to be f o |s|_y, |<s1,s2>|_y to be <|s1|_y,|s2|_y>, and |lam x.s|_y to be the transpose of |s|_{y,x:A}.

We can introduce the following abbreviations into this language: for g:B^A and s:A, write ev<g,s> as g(s) [notationally we may not be careful to distinguish between g(s) as gs formed from s:A and g:A->B and g(s) as ev<g,s> formed from g:B^A and s:A, but we should note that these are certainly different--there is a relationship between the two, however, obtained by using transposes]; for x:A and s:Omega, write "lam x.s" as {x:A|s}; for P:Omega^A and a:A, write "a in A" for ev<P,a> (which was previously abbreviated as P(a)); we can also abbreviate f(<s1,s2>) as f(s1,s2). We can also abbreviate and(phi,psi) as "phi and psi" and likewise abbreviate implication. "forall x:A phi" abbreviates forall_A{x:A.phi} (semantically, we take the transpose of |phi|_{y,x:A} and compose with forall_A:Omega^A->Omega). In the next chapter we define the other logical connectives and existential quantification (and false) in terms of these.

We can abbreviate "delta_A(a1,a2)" as "a1=a2" where a1,a2:A and delta_A:AxA->Omega classifies the subobject given by the diagonal arrow <1,1>:A>->AxA. Also, given monics i:I>->A and r:R>->AxB, we may abbreviate Chi_i(s) as I(s) and Chi_r(s1,s2) as R s1 s2.

Now, we can define "truth" using full subobjects. Also, we say a finite set of formulas Gamma implies a formula phi if the subobject [_x|Gamma] (i.e., the intersection of the subobjects given by each formula in Gamma) is contained in [_x|phi]. We can write this claim as the sequent Gamma:phi. If the sequent is true, then we write Gamma|-phi. Topos logic is given by rules of inference which yeild true sequents. The rules of inference are assumption (phi|-phi), truth (|-t), false (fa|-phi), thinning, substitution (Gamma:phi gives Gamma(x/s):phi(x/s)), cut (Gamma,psi:phi and Gamma:psi give Gamma:phi--with a free variable restriction on psi), and usual reversible rules for false (contradiction), and (in the succedent), or (in the antecedent--proof by cases), implication (in the succedent--the deduction rule), and the quantifiers. Also, we have the singleton axiom for the sort 1, the equality axioms (reflexivity and replacement), the biconditionality axiom ("v->w and w->v"|-w=v), the product axioms, the [functional] extensionality ("forall x:A.f(x)=g(x)"|-f=g), and the comprehension axiom (written here as |-(lambda x:A.s)x=s).

These rules are sound for any topos (as proven in the next chapter). Actually, since we have only defined conjunction, implication, and universal quantification (and truth), we only have to show these rules are sound. Then we define the other connectives, false, and the existential quantifier in terms of the language we already have and show that their rules are provable.

Topos logic is intuitionistic, not classical. In particular, we cannot prove excluded middle (phi or not phi), '--phi -> phi', nor can we prove '-(phi and psi) -> (-phi or -psi)' (half of one of DeMorgan's Laws). Also, the relationship between universal and existential quantification is not quite as trivial as in classical logic. We do not have '-(forall x.phi) -> exists x.-phi'. Also, since there are empty sorts, we do not have 'forall x.phi -> exists x.phi'. This can be summarized by saying, "it is hard to conclude from a negative, or to a disjunction or existential statement in topos logic."

On the other hand, we can prove noncontradiction in the forms '-(phi and -phi)' and 'phi -> --phi'. We can prove three of DeMorgan's Laws: '-(phi or psi) -> -phi and -psi', '(-phi and -psi) -> -(phi or psi)', '(-phi or -psi) -> -(phi and psi)'. The distributive laws of and and or are provable. As for quantifiers, we can prove '(forall x.phi) -> -(exists x.-phi)', '(exists x.phi)->-(forall x.-phi)', '(forall x.-phi) <-> -(exists x.phi)'. We can also prove some "local set theory" results, namely, there is an empty set for each object [sort], and we can form pair sets, power sets, and unions relativized to an object A.

Chapter 15: Soundness proof for topos logic. We can define false to be "forall w:Omega.w". This implies every formula by universal instantiation. We can define negation by "-phi" is "phi -> false". The deduction rule implies the reversible rule for negation. We can define "phi or psi" by "forall w:Omega.([(phi->w) and (psi->w)]->w)" where w is not free in phi or psi. This satisfies the reversible "proof by cases"-style rule (shown using the conjunction, deduction, universal instantiation, and cut rules). [The derivations verifying the "proof by cases"-style rule can be represented via the Curry-Howard correspondence by the lambda-terms (where I'm ignoring the free variables u:Gamma) "v:phi|-(Lambda w.lambda p:'(phi->w) and (psi->w)'.(pi1 p)v):'phi or psi'", "t:psi|-(Lambda w.lambda p:'(phi->w) and (psi->w)'.(pi2 p)t):'phi or psi'", and "r:'phi or psi'|-(<lambda v:phi.e,lambda t:psi.e'>(r theta)):theta" where e(v:phi),e'(t:psi):theta] Finally, we define "exists x:A.phi" as "forall w:Omega.((forall x:A.phi->w)->w)". We can show this satisfies the reversible rule for existential quantifiers using the cut, deduction, and universal instantiation rules. [Via the Curry-Howard isomorphism, these derivations correspond to the lambda terms (ignoring the full context Gamma) "x:A,v:phi|-(Lambda w.lambda r:'forall x:A.phi->w'.rxv):exists x:A.phi" and "t:'exists x:A.phi'|-(t theta (lambda x:A(lambda v:phi.e))):theta" where e(v:phi):theta and x is not free in theta.] So, if we show that the structural rules are sound and the rules for truth, conjunction, implication (deduction), and universal quantifers are sound, then it follows that topos logic with these definitions is sound.

First, we can prove the superfluous variable lemma which says that if s:A with free variables from the list _x=<x1:A1,...,xn:An> and we have any larger list of variables _y=<y1:B1,...,yk:Bk>, then |s|_y = |s|_x o <proj> where <proj> is the appropriate product of projection maps taking B1x...xBk to A1x...xAn. In terms of the extension of a formula phi, we have [y|phi] is the pullback of [x|phi] along <proj>. The same sort of proof verifies the substitution lemma, that |s(x/c)|_y = |s|_x o <|c|_y>. This tells us the extension of [y|s(x/c)] is the pullback of [x|s(x)] along <|c|_y>:B1x...xBk->A1x...xAn.

This can be used to show the substitution rule is sound. The other structural rules are sound simply by properties of inclusion and intersection of subobjects. The soundness of the cut rule follows (using the variable restriction so that every context for Gamma,phi is a context for Gamma,psi,phi) since Gamma|-psi implies [x|Gamma,psi] = [x|Gamma] and this with Gamma,psi|-phi implies [x|Gamma] <= [x|phi].

The conjunction rule is trivial to verify. The rule for implication (deduction rule) follows from the theorem in Chapter 13 which showed S intersect Q is smaller than R iff S is smaller than Q=>R. Finally, the rule for universal quantifiers (universal instantiation) is sound since, by the superfluous variable lemma, if y:A is not free in phi, then [_x,y|phi] = [_x|phi] x A. We use this with a theorem from Chapter 13 which stated that S is smaller than (forall a)R iff SxA is smaller than R.

Note that s1=s2 is true iff |s1|_x = |s2|_x. We use this to verify the reflexive and singleton axioms. The rest of the axioms follow with little difficulty.

Topos logic is complete in the sense that if a sequent is true in every topos, then it is provable in topos logic. Of course, it is not complete for a single topos.

not classifies fa. We can show this as follows. The internal language easily proves -w|-w=fa and w=fa|- -w. This implies the subobjects [w|-w] and [w|w=fa] are the same, hence they are both classified by not. But [w|w=fa] is the subobject fa:1->Omega because we can show <fa,fa> is the pullback of <<1,fa!>,<1,1>> (i.e., [x:Omega,y:Omega|x = y] has inverse image fa along <|w|_w,|fa|_w>:Omega->Omega x Omega). [This, for the most part, solves exercise 15.2 in McLarty, but this solution does not appear to be quite what he suggested.]

Since only and, implies, and universal quantification were defined categorically, and the rest of the logic was defined in the internal language, we should expect to use the internal language to prove properties of arrows induced by formulas. These results can then be translated into the topos.

Chapter 16: From the internal language to the topos. We can use the internal language and topos logic to prove facts about a topos. First, we have to translate basic concepts such as "monic" and "epic" (and so on) into the internal language. Then, we can prove epi-monic factorization for arrows, functional relations define arrows, and finite colimits exist.

First, note that for arrows f,g:A->B, f=g iff x.A|-fx=gx. An arrow f:A->B is monic iff x:A,x':A;fx=fx'|-x=x'. This follows since [x,x'|fx=fx'] is the kernel pair (subobject of AxA) of f, and the sequent holds iff the kernel pair factors through the diagonal iff f is monic (consider the pullback characterization of monic).

An arrow f:A->B is epic iff y:B|-(exists x:A.y=fx). To show this, we first show f:A->B is epic iff 1_B is the smallest subobject of B that f factors through. (If f factors through s:S>->B, then Chi_s o f = t_A = t_B o f = Chi_{1_B} o f implies Chi_s = Chi_{1_B} since f is epic. Conversely, if gf=hf, then consider the equalizer of g and h--f must factor through this--which implies the equalizer of g and h is 1_B, so that g=h.) Then we show that every f:A->B has an epi-monic factorization A--q-->>[y:B|(exists x:A.fx=y)]>->B. Consider the graph of f given by Gf=<1,f>:A->AxB, and the projection p2:AxB->B. Using the adjunction Sigma_p2:E/AxB->E/B -| p2*:E/B->E/AxB, we have an arrow Sigma_p2(Gf)->s iff we have an arrow Gf->p2*s for every subobject s:S>->B. Since Sigma_p2(Gf) = p2 o Gf = f, we have f factors through s iff Gf is a smaller subobject of AxB than p2*s. The graph of f is [x:A,y:B|y=fx] (simply check that Gf equalizes p2 o f and p1). Using the substitution lemma, [x:A,y:B|S(y)] is p*s. So, we have x:A,y:B;y=fx|-S(y) iff f factors through s. But since x does not occur free in the antecedent, we have (by topos logic) y:B;(exists x:A.y=fx)|-S(y) iff f factors through s. In particular, then, f factors through [y:B|(exists x:A.y=fx)]. This gives us the factorization A--q-->>[y:B|(exists x:A.fx=y)]>->B where q must be epic since it cannot factor through any subobject of [y:B|(exists x:A.fx=y)] smaller than the full one (any such subobject would give a subobject of B smaller than [y:B|(exists x:A.fx=y)]). So, we have f:A->B is epic iff the smallest subobject of B f factors through is 1_B iff [y:B|(exists x:A.y=fx)] is 1_B iff y:B|-(exists x:A.y=fx).

The epi-monic factorization also implies x:A|-I(x)<->(exists w:I.x=i(w)) for all monics i:I>->A. The point is that I is the smallest subobject i can possibly factor through, hence must be [x:A|(exists w:I.x=i(w)]. Applying this to relations r:R>->AxB, we have x:A,y:B|-R(x,y)<->(exists w:R.<x,y>=r(w)).

Every relation r:R>->AxB factors as arrows <h,k> (neither of which must be monic). The arrow h is iso iff r is equivalent to the graph of some arrow f:A->B, and that arrow must be f = k o h^{-1}. (This holds in any category with binary products.) We call a relation "single-valued" if x:A,y,y':B;Rxy,Rxy'|-y=y'. If R is single valued, then h is monic. (Assume h o c = h o d, use single-valuedness to show k o c = k o d so that r o c = r o d which implies c=d.) A "totally defined" relation R is one for which |-(forall x:A.exists y:B.Rxy). If R is totally defined, then h is epic. (The sequent for totally defined is equivalent [by above] to |-(forall x:A.exists y:B.exists w:R.<x,y>=r(w)). From this sequent (by composing both sides of the equation by the first projection), we can prove |-(forall x:A.exists y:B.exists w:R.x=h(w)). Since y no longer occurs in the scope of its quantifier, we can eliminate this quantifier to obtain |-(forall x:A.exists w:R.x=h(w)). But this is precisely the internal language way of saying h is epic.)

A relation r=<h,k>:R>->AxB is "functional" if it is both single-valued and totally defined. By above, such a functional relation must have h monic and epic, hence iso. So, r is equivalent to the graph of a unique function f:A->B. That is, functional relations define arrows!

We sometimes define arrows to and from subobjects determined by extensions [x:A|phi]. Let d:D>->A be this extension. Then, we have y:D|-phi(d(y)). (The pullback of d along d is 1_D, and by the substitution lemma, [y:D|phi(d(y))] is the pullback along d of d=[x:A|phi(x)].) Also, an arrow f:B->A factors through [x:A|phi] iff y:B|-phi(f(y)). (In any category, f:B->A factors through a subobject s:S>->A of A iff 1_B is the pullback of s along f [even more generally, f = g o h iff <h,1> is the pullback of <f,g>]. By the substitution lemma, [y:B|phi(f(y))] = f*[x:A|phi(x)]. These facts give the result.)

[y:1|fa] is some 0>->1. By definition, we have this classified by fa:1->Omega. We can show 0 is initial (so that every topos has an initial object). First, we show that if any sequent contains a free variable x:0, then the sequent is true. The key point is that we have x=x|-fa for x:0 (since both subobjects [x:0|x=x] and [x:0|fa] are 0>->0--draw the pullbacks). We can use this with the cut rule to obtain a proof for any Gamma:phi where x occurs free. The free variable restriction on the cut rule prevents us from using the same procedure to prove any Gamma:phi. Now, we can show 0 is initial by noting that each identity relation 0xA->0xA is functional (since the sequents which prove it is functional contain free x:0), and so defines an arrow 0->A. Also, for any two arrows h,k:0->A, the sequent which says h=k is true because it contains a free x:0.

Note that we cannot have any arrows into 0 (it is a strict initial object) since a topos is a CCC (so arrows out of 0 are monic). The pullback defining 0 says that fa is disjoint from t. We know that not:Omega->Omega classifies fa:1>->Omega. So, if not o y = t!, then y = fa! (in particular, -t = fa). A truth value with negation true must be false.

Also, -t = fa. We can see this in the internal language by noting fa -||- t->fa. In terms of subobjects, we can see this by noting both [y:1|-t] and [y:1|fa] classify 0>->1 (use the pullback lemma to combine the pullbacks with fa classifying 0>->1 and with not classifying fa).

However, -w = fa does not necessarily imply w = t. We do have -w = fa implies --w = t (since w->fa = fa can be used to prove (w->fa)->fa in an obvious way).

An object C is a coproduct of A and B with (monic) injections i1:A>->C and i2:B>->C if the sequents w:C|-'A(w) or B(w)' and w:C|- -(A(w) and B(w)) are true. (A functional relation defines the unique arrow u:C->D for every pair f:A->D, g:B->D.) For any A and B we can find such a C with i1:A>->C and i2:B>->C by starting with monics <{},empty!>:A>->Omega^A x Omega^B and <empty!,{}>:B>->Omega^A x Omega^B (monic since each {} is). We can factor these monics through [Q:Omega^A x Omega^B|(exists x:A.Q=<{x},empty>) or (exists y:B.Q=<empty,{y}>)]:C>->Omega^A x Omega^B, giving monics i1:A>->C and i2:B>->C which compose to give the original two monics. The two sequents which assert C, i1, and i2 form a coproduct of A and B follow. So, every topos has binary coproducts. In fact, they have binary coproducts where the injections are monic and disjoint.

In order to conclude that every topos has all finite colimits, we need to show the existence of coequalizers. First, we study equivalence relations in a topos.

In the internal language, the sequent |-cy = cy' <--> Ryy' holds iff <h,k>:R>->BxB is the kernel pair of c:B->C. (Consider the extension of cy=cy' and the equivalence between the kernel pair pullback and the pullback giving the extension of cy=cy' via the substitution lemma.) Every equivalence relation <h,k>:R>->BxB is the kernel pair of some epic q:B->>Q. This q is the epic part of the epi-monic factorization of the arrow I:B->Omega^B defined by |{w:B|Ryw}|_{y:B} (intuitively taking each member of B to its equivalence class). We can show that this q satisfies the sequent above. Now, every epic is a coequalizer for its kernel pair. (We can define the unique u given by the universal mapping property by a functional relation.)

So, we have shown that each pair of arrows <h,k> forming an equivalence relation has a coequalizer. Given any two pairs of arrows f,g:A->B, define the subobject of Omega^{BxB} of equivalence relations which respect f and g. We can use this to define the smallest equivalence relation (subobject of BxB) which respects f and g. Write this equivalence relation as <h,k>:R>->BxB. We can show that for any c:B->C, c o f = c o g iff c o h = c o k (since for any c we have c o f = c o g iff the kernel pair of c respects f and g iff R contains the kernel pair relation of c iff c o h = c o k). This (by a basic categorical argument using nothing special about toposes) implies that any coequalizer of <h,k> is a coequalizer of <f,g>. So, every pair of parallel arrows in a topos has a coequalizer.