FOM: Reply to Mossakowski on category theory

[Joe Shipman]

Thanks for clarifying the issues so well.  What I am interested in is
applications of category theory to topology, number theory, etc.; is
there a single application of, say, the Yoneda embedding theorem which
can't straightforwardly be redone in ZFC?  If not, why isn't there a
metatheorem to this effect?  Obviously the one-universe assumption is
not conservative over ZFC, but has anyone tried to determine whether the
Yoneda embedding theorem (or a similar theorem about categories which
needs more than VNBG) is conservative over ZFC?  Is Morse-Kelley set
theory sufficient to prove the Yoneda embedding theorem?  If not,
exactly what theory was this "theorem" proved in?

It is hard for me to believe no one has tackled these well-defined
questions.  It is posible that in the general setting the Yoneda
embedding theorem for small categories may require an inaccessible, and
the general Yoneda embedding theorem may require a proper Class of
inaccessibles, but THIS IS AN OPEN QUESTION and someone should be
working on it!  In the specialized setting of applications to sets of
rank less than omega+omega, it is very important to know whether
Yoneda's theorem is conservative over ZFC.

About the only thing McLarty and Simpson agreed on was that the
Tarski-Grothendieck Universes assumption could be eliminated from
applications of derived functor cohomology to number theory; but nobody
was willing to state a metatheorem, so we must depend on ad hoc
arguments in each case.  In the same way, I'd like to see a metatheorem
of the form

(*) Any statement about integers proved using the Yoneda lemma is a
theorem of ZFC if the proof was such that {insert a definability
condition about the functors involved, or a smallness condition about
the categories used, or whatever}.

Even better would be the simpler

(**) Any statement about integers proved using the Yoneda lemma is a
theorem of ZFC

-- will category theorists reading this at least hazard an opinion on
whether (**) is true, or conjecture a precise form of (*)?

-- Joe Shipman