I have been thinking on how to get this post right for a few days, taking my time, but André's recent post
Can we define a notion of (large) category without supposing that its (large) set of objects has a diagonal?
prompted me to send this... perhaps prematurely. One can do a lot of mathematics without using the equality predicate. The necessary technology (dependent types) has been around for a long time, and the foundations of category theory is a natural domain of application for it. Richard Gardner has already said something to that effect, but I want to stress that point and try to sell it to the less syntactically inclined among us. In dependent types you still need a very limited form of equality, to be able to compare syntactic objects. After all, if you make a complex syntactic construction A, you have to be able to make copies of it and reuse it elsewhere at several places, and you want your theory to take account of this. And, more importantly, if you start with A and elaborate on it twice, getting two syntactic objects S(A), T(A), it is natural to be able to assert that the two results are equal, because some times they will. The standard example of this is beta- reduction in the lambda calculus. But as I said this is a very limited form of equality, since a true equality predicate would allow you to assert if two *arbitrary* objects are equal. The syntax of dependent types is rather heavy, but once you know how to interpret it in a category C it is very intuitive. To get started all you need is a class of maps in C which is stable under pullbacks. and then you interpret such a special map A: \bar A ----> X as a dependent type x: X |- A(x) I.e., if types in say, simple lamda calculus can be interpreted as sets (or spaces), then dependent types can be interpreted as an indexed family of sets, depending on another set. The operation of pullback is substitution of a term in a type. That is, if an aribtrary map B ----> A in C is thought of as a term, in the usual Lawvere-Lambek sense b:B |- f(b) then the pullbakck of A by f represents the type b:B |- A(f(b)) Most of the people on this list are already very familiar with this *intuition*, which has been used countless times since the mid-fifties starting in algebraic topology, then algebraic geometry, then categorical foundations (I mention in particular the idea of using such a class of pullback-stable maps in a topos-like category as a notion of smallness, introduced (i think) by Bénabou and used extensively by Joyal-Moerdijk in a monograph, and lots of other people who are reading this list. But the point of this post is that I think there is still the need to stress that there is a *formal syntax* which corresponds to this intuition, although many people on this list are already aware of this. We have learned to "reason intuititionisticallty" in a topos, and intuitionistic predicate theory was a real help in doing so... the same goes here: we can learn to reason in situations where the equality predicate is limited to special types, the *discrete* ones. And this point it is easy to illustrate. Let us go back to our category C. People have known for a long time that all you need to do to define internal categories in C is to require that C have pullbacks. But actually the natural requirements are even weaker: all you need is that C have a special class of maps closed under pullbacks (and that includes all isos). For simplicity today I will also require a terminal object. As I already said you think of these maps as indexed families. So suppose X is chosen to be the object of objects of an internal category. You want a family of morphisms. I.e., given the usual span d_0 : X <----- H -----> X d_1 it is now required that X ---> 1 be one of these special maps (so that "X is an independent type") and both H ----> X are required to be special maps too. It is easy to see then that <d_0, d_1> : H -----
X x X is also a special map. We can now say that these two maps define an indexed family:
x: X, y: X |- Hom(x,y) Now look at how composition is presented: x,y,z : X , h: Hom(x,y), k: Hom(y,z) |- k o h : Hom(x,z) This is intepreted in C via very mechanical constructions, which will give the interpretation of composition as the usual map, with the usual pullback as source and which obeys the usual commutation requirements. Notice that the syntax we used *does not need an equality predicate to assert that dom(k) = cod(h)* The same goes with the identity map x: X |- Id(x) : Hom(x,x) But now look at associativity: x,y,z,w: X, h: Hom(x,y), k: Hom(y,z), g: Hom(z,w) |- g o (k o h) = (g o k ) o h Here you need a real equality predicate. That means that the sets in the indexed family (Hom(x,y))_x,y are required to be *discrete sets*, i.e., that the diagonal is required to be a predicate. There is some leeway on how to define predicates, but a natural way to do it is to say that predicates are (represented by) special maps that are monos. Thus, to be back to the "small is beautiful" track, a first approximation of Large/Small goes (very roughly) space/discrete space. Several years ago i circulated a manuscript where I was trying to formalize foundations of category theory by specializing the space/ discrete space duality above to groupoid/discrete groupoid. I was using fibrations of groupoids over a base category (potentially a topos) as a reference model. In other words, I was trying to find the kind of elementary toposes you would get if you subsituted fibrations (and stacks) of groupoids for presheaves (and sheaves). I made some very interesting observations, but one problem I hit was that these categories are only bi-cartesian closed, not cartesian closed, and that really stretched the available syntactic technology. It seems that you can't avoid going in higher dimension whenever you tackle such issues. I was using groupoid-enriched categories as the basic language of my axiomatization. In other words, a class comes *indissociably equipped* with a notion of isomorphism between its objects, and only discrete classes have the true equality predicate. The point is that the classes that you first meet in real life are classes of sets-with-structure, and that *if you have properly defined a structure, you should know what the isomorphisms are*. Moreover, whatever you do to a mathematical object, you should be able to transport along an isomorphism. Naturally I got the idea from André's theory of combinatorial species. This is perfectly in accordance with dependent type theory: you don't have to know when two structures are equal; what really matters is having an iso between them, because then they are interchangeable. So I was working on the principle that all the constructions usually done on sets should be lifted to groupoids, which then always allow you to use transport on whatever you've constructed. But another problem I hit was that the powerset construction is very much weakened, because given a groupoid X, the only natural notion of PX is the (discrete) class of all subgroupoids that are isomorphism-closed ("replete"). This weakens the logic very much and you cannot use higher-order logic to do things like constructing sums, as in elementary toposes. But you sitll can interpret a form of predicate logic in there. Naturally a predicate in general is interpreted as a replete subobject, which is quite natural. A property only makes sense only if it is invariant under iso. The use of subobjects as predicates show that his approach is more aligned with Church-style intuitionism than Martin-Löf-style constructive foundations. One of these interesting observation that I made is that there is a special version of the axiom of choice in that context, which is perfectly suited for category theory, but does not clash with constructivism. And it is valid in fibrations and stacks. Presented in ordinary categorical language, it goes: given a class/groupoid G and a family of classes that depend on it (a fibration of groupoids over G in the ordinary sense) such that every class/fiber of the family is inhabited (which is surjective as a fibration) and such that all theses fibers are *equivalent to discrete sets* (in other words such that hom-sets are never bigger than singletons, Bénabou has a name for these) then the fibration has a splitting. This is the axiom of choice that categorists use all the time: universal constructions give rise to exactly such fibrations---existence up to uniqueisomorphism---and they are the cases when the axiom of choice is needed. Richard mentions some foundational work that I was not aware of, where the higher-order categories go all the way up to tri. It seems that this particular case of dimension-climbing is a formal consequence of the base axiomatics, while mine came from semantics. But I think we should seize the bull by the horns and base foundations on higher- dimension groupoids (i know that other people on this list agree, and I should mention Makkai's opetopes). Because naturally after you've consider classes of sets-with structure, you cannot avoid getting (meta?)classes of classes-with-structure, where isomorphism has become equivalence, und so weiter. To go back to André's original question: you can build foundational universes whose inhabitants are groupoids and ordinary not sets/ classes in general. The diagonal in these will exist *but it will not be a predicate*. Hope this isn't too ponderous, François [For admin and other information see: http://www.mta.ca/~cat-dist/ ]