Re: Not invariant but good

[Michael Shulman <shulman@math.uchicago.edu>]

On Fri, Oct 1, 2010 at 2:24 AM, Thomas Streicher
<streicher@mathematik.tu-darmstadt.de> wrote:
> Well, but then we can work with categories with a chosen structure, e.g.
> chosen products; that's what is recommended in the Elephant and it looks to
> me as close to practice; it's very unlikely to have a nonconstructive proof
> of existence of products.

Unlikely, but it happens occasionally.  For instance, if the morphisms
of a category are equivalence classes, then a "construction" of
equalizers or pullbacks might require choosing representatives; this
actually happens at one point in the Elephant.  The "small complete
categories" in realizability topoi are also generally "weakly
complete," in the sense that "every small diagram has a limit" is true
in the internal logic, but not "strongly complete" in the sense that
there exist internal limit-assigning (non-ana) functors.  The property
of "strong completeness" is also not in general preserved or reflected
by weak equivalence functors.

One can of course develop a theory which distinguishes between weak
and strong equivalence and weak and strong completeness, but I think
it's reasonable to call it "unfamiliar" to most category theorists.
It feels to me like trying to do work constructively with topological
spaces and therefore having to talk about [0,1] being complete and
totally bounded but not compact, instead of realizing that when
working constructively, one should really replace topological spaces
with locales.  Just as in set theory, no axiom of choice is necessary
to define a function whose values are individually uniquely
determined, it seems to me that no axiom of choice should be necessary
in category theory to define a functor whose values are individually
uniquely determined up to unique isomorphism.  But obviously this is a
subjective judgement.

Mike


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]