Categorical Foundations of Mathematics?

[Timothy Y. Chow]

Harvey Friedman wrote:
> Furthermore, at least so far, category theory hasn't even been useful 
> for ANY of our dramatic foundational revelations, of which we have a 
> few. The really useful tool for uncovering the dramatic foundational 
> revelations has always been through the usual standard classical set 
> theoretic foundations.

While it might not count as "dramatic," the fact that a certain segment of 
homotopy theory ("synthetic" homotopy theory), which at first glance seems 
to require rather strong set-theoretic axioms to formalize (universes), 
actually requires much less proof-theoretic strength (some kind of 
Martin-Lof type theory or Kripke-Platek set theory) was discovered by 
thinking hard about foundations from the point of view of higher category 
theory and type theory.

The above point has been mentioned before on FOM, but perhaps was obscured 
by confusing debates about "homotopy type theory as a foundation for all 
of mathematics" and the relationship between "synthetic" homotopy theory 
and conventional homotopy theory.  But if we lay such debates aside and 
just focus on the reverse mathematics, it seems to me to be a clear case 
in which not only was the insight historically arrived at via 
non-set-theoretical methods, but where conventional set-theoretic thinking 
may have posed a psychological barrier to making the discovery.  The 
conventional thinker might object to referring to an argument as a 
"computation of the homotopy group of a sphere" unless that statement is 
interpreted in terms of conventional homotopy groups of conventional 
spheres, and that might present an obstacle to analyzing the logical 
structure of the argument on its own terms.

Tim