Internal anafunctors.

[Toby Bartels <toby+categories@math.ucr.edu>]

Has anybody worked out a theory of internal anafunctors?


On the one hand, there is a notion of internal category,
that is a category internal to some other category,
such as (were these the first?) Ehresmann's differential categories.
There are also (I assume that Ehresmann discussed these too)
internal functors between these internal categories.
In particular, one component of an internal functor from X to Y
is a morphism from the object of objects of X to the object of objects of Y,
just as one component of an ordinary functor from C to D
is a function from the set of objects of C to the set of objects of D.

On the other hand, Marco Makkai has argued that,
if you don't believe in the axiom of choice
(either because you disbelieve or wish to be agnostic),
then you should use anafunctors (possibly always saturated)
instead of functors in general category theory.
In particular, an anafunctor from C to D does *not* necessarily include
a function from the set of objects of C to the set of objects of D
(although such a function does follow from the axiom of choice).

Now, even if you believe in the axiom of choice,
still there are many topoi in which choice does not hold.
Yet Makkai's theory of anafunctors (being constructive)
can be expressed in the internal language of a topos,
so there is automatically a theory of internal anfunctor
between internal categories in an arbitrary topos.
(Arguably, this should be regarded as the right way
to internalise category theory into a topos,
or more generally to treat models of constructive category theory.)

My question, then, is whether anybody has worked this out
in arbitrary categories, or at least more generally than in topoi
(for example, in an arbitrary site).  In particular, has anybody worked out
differentiable anafunctors between differentiable categories
(internal to the category of differentiable spaces)?


I am pretty sure that I know how to do this,
and it will be used in my PhD dissertation.
But I would prefer to give the proper credit,
and even replace as many proofs as possible
with citations to others' papers! ^_^


-- Toby Bartels