FOM: Circular 2-CAT foundations

[Till Mossakowski]

Vaughan Pratt wrote:
> As a formalism for categorical foundations sketches have the same
> weakness as Colin's axiomatization of categories: they are based
> on ordinary categories, with no 2-cells.  (Again let me stress the
> importance of 2-categories, i.e. not just line segments but surface
> patches, for foundations.)  On the one hand I'm sure this is not an
> intrinsic limitation of sketches, on the other I don't know what's been
> done along those lines to date.  Higher-dimensional sketches are surely
> well worth pursuing.

That's true. If we take McLane's slogan "Adjoints arise everywhere"
seriously, in a categorical foundation, adjunctions should be a
primitive or easily derived notion, and this requires a 2-categorical 
setting.

So a truely circular category theoretic foundation would replace
first-order logic with a sketch-like formalism, with primitive 
notions like limits, colimits and adjunctions, replacing quantifiers 
and connectives. This formalism would be interpreted in naive 2-category 
theory,
comparable to first-order logic being interpreted in naive set theory.
(The existence of a "naive 2-category theory" may be questioned, but
relying on naive set theory may be the cause for the "slavish 
translastions".
Or with Vaughan Pratt's (Feb 25th) words: if you want to explain glue
and 
use sand to build the glue, then the glue can become an important 
principle of organizaiton, but the foundation is still sand.)

Then, using such a formalism, the second part of the challenge would be
to 
axiomatize the 2-category of 2-categories in a way that gives a formal 
analysis of not only the naive notions that have been assumed, but also
of (a considerable part of) mathematics. This would play the role of
ZFC.

While almost all fundamental notions of category theory can be
formulated 
in an arbitrary 2-category, the notion of "weak" identity (understood as 
"isomorphism up to (isomorphism up to (isomorphism up to ... ))")
may be an important exception. If you really needed to fully grasp this
(say, with weak n-categories or \omega-categories), then a categorical
foundation possibly would have to wait for easier formulations
of higher-dimensional category theory.

Till Mossakowski