Re: equality is beautiful

[Michael Shulman <shulman@uchicago.edu>]

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/ ]