categories: functors up to isomorphism

[Paul Taylor <pt@dcs.qmul.ac.uk>]

An account of "functors defined up to isomorphism" of the kind
that David Benson suggested was given by Michael Makkai in
   "Avoiding the axiom of choice in category theory",
JPAA 108 (1996) 109--73, under the name "anafunctors".

This theory is one to which the quotation attributed to Voltaire
is applicable: I disapprove of what Makkai says, but would defend
to the death his right to say it (or at least give him a pat on
the back for having the stamina to work it out).

One reason for disapproval is being accused of using Choice.

For definiteness, suppose that the functors that interest us are
product and function-space, and that the objects of our category
are topological spaces.  Then if I say that a certain category of
spaces is cartesian closed, I am allegedly invoking Choice to make
a once-and-for-all assignment of the manner of construction of
the products and function-spaces of all pairs of spaces.

Whilst it is correct to observe that these constructions are defined
(by their universal properties) only up to unique isomorphism,  the
same observation needs to be taken a step further:
   the category of spaces is only defined up to equivalence,
and therefore
   we may freely replace the God- or ZF-given category
   by one that is more convenient for us!

The root of the dispute between those that consider (objects and)
functors to be defined "on the nose" or only up to isomorphism is the
cultural dichotomy between syntax (computer science) and semantics
(mathematics).  Having recognised that dichotomy, we can bridge it.

Much as mathematicians enjoy the conceit that they're manipulating
genuine (often infinite) objects, in reality ALL that we can ever do
is to push around symbols.  In particular, when I write XxY or X->Y,
that is ALL that I do: I don't treat God as an odd-job man and make Him
shift uncountable tangles of curly brackets and Choose things for me!

More prosaically, the given category of spaces provides the base types
and constant terms in a calculus, and each expression XxY or X->Y is
just that - an expression in the calculus.  These type- and term-
expressions are the objects and morphisms of another category, which
is equivalent to the original one, but has the useful property of
carrying an assignment of products and function-spaces.

In fact, there is a functor from the original "semantic" category to
the new "syntactic" one that (under suitable conditions) is full,
faithful and essentially surjective, ie a weak equivalence. It has a
pseudo-inverse (making it a strong equivalence) iff the original
category has an assignment of products and function-spaces: this is
where the Choice comes in - or may be avoided.

The construction of syntax from semantics is written up in Section 7.6
of my book, "Practical Foundations of Mathematics" (CUP, 1999)
    http://www.dcs.qmul.ac.uk/~pt/Practical_Foundations/html/s76.html
where the word "canonical" is adopted from sheaf theory, and there
is an example of a situation where proving naturality of a certain
family of maps is the crux of an argument.

Paul Taylor
(no academic affiliation).