equality is beautiful
Dear All Many people seem to distrust the equality relation between the objects of a (large) category. Is this a philosophical conundrum or a mathematical problem? Can we define a notion of (large) category without supposing that its (large) set of objects has a diagonal? Best, André [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
On 9 Jan 2010, at 03:29, Joyal, André wrote:
Dear All
Many people seem to distrust the equality relation between the objects of a (large) category. Is this a philosophical conundrum or a mathematical problem?
Can we define a notion of (large) category without supposing that its (large) set of objects has a diagonal
Dear Andre, Can I explore this with regard to topologies? Suppose we compare FinSet with Set, defining FinSet very small with N for its object space. The object diagonal N -> NxN is an open inclusion. Now look at Set. The natural topology on the class of sets, as the Ind-completion of FinSet, is the one whose sheaves are given by the object classifier. Thus continuous maps from it are functorial and preserve filtered colimits (the categorical analogue of Scott continuity). (This introduces a confusing issue. Functors from the category Set are already determined by their object maps. But it is a special category in which the morphism space is the comma object got from two copies of the identity map on the object space - we are using the fact that the category of spaces is actually a 2-category, using the specialization morphisms. FinSet was certainly not of this kind.) Now the object diagonal is not even an inclusion, since it is not full. I would speculate, by analogy with what I know for ideal completions, that it is essential but not locally connected. I don't really know what to make of this, but it does seem that there are topological distinctions to be made between the two categories based on object equality. Now let me wonder about classifying toposes. I love using them (as I did above), but they always seem slightly fuzzy because they are really defined only up to equivalence. So I certainly would distrust the object equality. I think the discussion becomes slightly sharper in terms of arithmetic universes (as mentioned by Paul Taylor) instead of toposes. Given a base AU A0, there are two obvious places to look for an object classifier (representing the class of sets) a la Grothendieck topos theory. First, there is A0[U], the AU freely generated over A0 by an object U. This can be constructed by universal algebra, and then is a classifying A0-AU (for the theory with one sort and no predicates, functions or axioms) characterized up to isomorphism with respect to strict A0-AU homomorphisms. However, its object equality depends rather delicately on the precise structure used to characterized AUs. For example, I suspect it will differ according as AUs are taken to have canonical pullbacks or canonical binary products and equalizers. On the other hand, sheaf theory would suggest using the category Presh (FinSet^op) of internal diagrams over the internal FinSet in A0. I conjecture that this (is an AU and) is equivalent but not isomorphic to A0[U]. Hence there are issues of object equality when one compares them. (Milly Maietti and I are looking at "subspaces" in this AU setting, and again are having to be rather careful about equality and the distinction between strict and non-strict AU homomorphisms.) A further issue, seen in AUs but not toposes, is that A0[U] can be internalized in A0, as the internal AU in A0 freely generated by one object. The comparison with the external A0[U] will presumably raise truth v. proof issues similar to those that you have already investigated for the initial AU and Goedel's Theorem. To summarize: (1) Granted the existence of the object diagonals, they may still have different topological characteristics for different kinds of categories. (2) A universal characterization (such as for classifying toposes) that is only up to equivalence will make it difficult to rely on object equality. (3) In arithmetic universes we can perhaps (allowing for the fact that the theory is not fully developed yet) see situations where the object equality definitely exists, but is sensitive to inessential differences. Best regards, Steve Vickers. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Joyal wrote:
Many people seem to distrust the equality relation between the objects of a (large) category. Is this a philosophical conundrum or a mathematical problem?
I don't even trust it for the *-autonomous category with two objects and three morphisms. This is the basis for the classical notion of truth as normally understood when not trying to parse the sentences of constructive mathematicians. Some dark night someone could sneak into the basement where the foundations of mathematics are stored and switch true and false around, and in the morning we'd all wake up talking Doublespeak without even realizing it. Are you suggesting we should trust the equality relation between the objects of that category? Useful categories don't come much smaller. It can't be a question of size because the free Heyting algebra on one generator is infinite yet it doesn't have this structural ambiguity of classical logic: we can trust its equality relation because we can tell which element is the generator even if the arrows are accidentally flipped---it's a sort of error-detection feature of that Heyting algebra not possessed by any Boolean algebra. This is a reason to prefer intuitionistic logic over classical (not one I'd use myself mind you). Best, Vaughan [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear André
Many people seem to distrust the equality relation between the objects of a (large) category. Is this a philosophical conundrum or a mathematical problem?
Can we define a notion of (large) category without supposing that its (large) set of objects has a diagonal?
Yes, this is precisely what one does in formalising category theory in an (intensional) dependent type theory. (Mike Shulman has alluded to this in a previous message to this list.) Since in such a type theory one does not have quotients of equivalence relations, one typically works not with raw types but with setoids (=types equipped with an equivalence relation in the internal logic). The category of such setoids is well behaved---at least an LCC pretopos---but the notion of internal category in this pretopos is generally not what one is interested in. Instead one takes a category internal to the type theory to be given by a type of objects O, together with an OxO indexed family of hom-setoids O(x,y), composition and identities which are maps of setoids, and associativity and unitality witnessed by elements of the hom-setoid equality. In this setting, we may not talk of equality of objects (since O is not a setoid but only a type) but may talk of the equality of any pair of parallel arrows. This notion is due to Peter Aczel and there is a fairly extensive development of it in the proof assistant Coq by Gérard Huet and Amokrane Saïbi. Some consequences of the definition are, e.g., that the collection of all small categories does no longer forms a category, but only a bicategory (since one cannot speak of equality of functors, since this would require equality of objects in the codomain). Some work on this has been done by Olov Wilander. Since the category of sets is a model of extensional, and so also intensional, type theory, one may interpret what the above means in this context to obtain, within a classical (or at least impredicative) metatheory, a notion of category meeting your requirements. In fact such non-standard categories may be seen as special kinds of tricategory (in the usual sense). Indeed, in the set-based model of type theory, a setoid is given by a set X; for each pair of elements x,y in X, a further set X(x,y); and arrows of composition X(y,z) x X(x,y)-->X(x,z), inverse X(x,y)-->X(y,x) and identity 1-->X(x,x) subject to no axioms. But this is precisely to give a bigroupoid which is locally chaotic, in the sense that between any two parallel 1-cells, there is a unique 2-cell. [From a constructive perspective, not every such bigroupoid would be "OK". The constructively valid ones would be the cofibrant ones, since these may be inductively generated.] From this it follows without difficulty that a category in the constructive sense is precisely a tricategory (in the sense of Gordon-Power-Street) whose every hom-bicategory is a locally chaotic bigroupoid. The use of these non-standard categories is pertinent with regard to Bill Lawvere's comments on the distinction between presentations and the things (theories) that they present. There is a model structure on the category FPCat of small categories with chosen finite products and strict product-preserving maps whose cofibrant objects are, up to retracts, the (many-sorted) Lawvere theories. One may define, in a similar way, a category FPCat' whose objects are non-standard categories with finite products, and whose morphisms are strict structure-preserving maps: and on this there is a model structure (or at least the cofibration-trivial fibration half of a model structure) whose cofibrant objects are "equational presentations of Lawvere theories": one has not only the sorts, and the generating operations, but also the generating equalities between composite operations. There is an adjunction between FPCat and FPCat' which is the left-hand of the two adjunctions described by Bill. Richard [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
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/ ]
This whole discussion has been very instructive to me, especially by showing that the same fundamental ideas have occurred to many people over and over again, but seemingly never quite made it out into the general mathematical consciousness. (Either that, or else I've completely missed them.) lamarche wrote:
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.
I would be interested in seeing this manuscript, because it sounds like exactly the same direction that some people have recently been trying to work on "higher-dimensional type theory" and 2-topos theory. For instance, Richard Garner's paper on "two-dimensional type theory" (http://www.dpmms.cam.ac.uk/~rhgg2/2-LCCC/2-LCCC.html) sounds almost exactly like the type theory you are describing, with categories for which Hom(x,y) is a "discrete set", i.e. has a diagonal that "is a predicate" (i.e. is "extensional"). He also deals with an "intermediately weak" form of cartesian closure for 2-categories. A number of people have also recently been thinking about 2-dimensional analogues of elementary toposes. On the one hand, there is Mark Weber's work on "2-toposes" which of course uses "strict" cartesian closure. I have been thinking from a different direction, starting from Street's characterization of "Grothendieck 2-toposes" with Giraud-like exactness axioms, using those exactness axioms to describe an internal logic/type theory for a "2-pretopos" which contains "hom-objects" that are "discrete"---whereas not every object is discrete. (A very preliminary version of this can be found here: http://ncatlab.org/michaelshulman/show/2-categorical+logic .) It generally seems to me that most "first-order" properties of elementary toposes generalize quite well, whereas those that use power objects are touchier.
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.
I agree entirely. In fact, I would argue that this is not really a version of the axiom of choice at all, but rather a principle of *functor comprehension*. In ordinary set theory, the axiom of choice is not necessary in order to make choices that are uniquely determined. This is sometimes called the "axiom of unique choice" or "axiom of non-choice" or the "function comprehension principle." In categorical language, it corresponds to the fact that any morphism which is both monic and strong epic must be an isomorphism (in a pretopos, of course every epic is strong). This makes the most sense to think about in a regular category, which has stable (strong epi, mono) factorizations, and the function comprehension principle is true in the internal logic of any such category. Likewise, in category theory, the axiom of choice "should" not be necessary in order to make choices that are uniquely determined up to unique specified isomorphism. The fact that an axiom of choice *is* required for such "choices" in standard set-theoretic foundations of category theory I would regard as merely a defect of those foundations. (This defect can, however, be worked around by using "anafunctors" instead of ordinary functors.) Another way of stating the "functor comprehension principle" is that any fully faithful functor (between groupoids, or even between categories) which is surjective on objects must have a section, or equivalently that any functor which is fully faithful and essentially surjective must be a (strong) equivalence. In 2-categorical language, this corresponds again to saying that any map which is both "monic" and "strong epic" must be an equivalence. Here we define a morphism in a 2-category (or bicategory) to be "monic" if it is "fully faithful" in the representable sense (perhaps this should be called "1-monic" for disambiguation with morphisms that are merely "faithful"), and "strong epic" (or "strong 1-epic") if it is left orthogonal to monics (in the bicategorical sense). In Cat, the monics are the fully faithful functors, and the strong epics are those that are essentially surjective on objects. In his paper "A characterization of bicategories of stacks," Street observed that Cat is a regular 2-category, i.e. it has good stable (strong epi, mono) factorizations. The functor comprehension principle is of course true, for the same tautologous reasons, in the "internal logic" of any regular 2-category, suitably defined. However, the fact that Cat is a regular 2-category (and in fact, the characterization of strong epics in Cat as e.s.o. functors) depends on the axiom of choice. But surely AC "should" not be necessary for Cat to be a regular 2-category, just as AC is not necessary for Set to be a regular category. This can be remedied with anafunctors: the bicategory of categories and anafunctors is always regular, whether or not we assume AC. Alternately, however, we could assume in our foundational axioms "Cat is a regular 2-category" or better a "2-topos," instead of a set-theoretic axiom system about Set, and get the functor comprehension principle automatically (and without implying any form of AC). Best, Mike [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (6)
-
Joyal, André -
lamarche -
Michael Shulman -
Richard Garner -
Steve Vickers -
Vaughan Pratt