From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5521 Path: news.gmane.org!not-for-mail From: Michael Shulman Newsgroups: gmane.science.mathematics.categories Subject: Re: equality is beautiful Date: Wed, 13 Jan 2010 15:29:06 -0600 Message-ID: References: Reply-To: Michael Shulman NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1263478356 3417 80.91.229.12 (14 Jan 2010 14:12:36 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Thu, 14 Jan 2010 14:12:36 +0000 (UTC) To: lamarche , categories@mta.ca Original-X-From: categories@mta.ca Thu Jan 14 15:12:28 2010 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1NVQR1-0001Z0-Cp for gsmc-categories@m.gmane.org; Thu, 14 Jan 2010 15:12:27 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1NVPxu-0002DJ-2s for categories-list@mta.ca; Thu, 14 Jan 2010 09:42:22 -0400 In-Reply-To: Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5521 Archived-At: 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 i= n > 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=E9nabou has a name for the= se) > 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/ ]