Vaughan has hit the nail on the head as far as computer science goes. The object-morphism analysis is such a good match for types and functions in programming languages, especially functional programming, that there is now a lot of applied category theory going on in computer science departments. The universal characterizations of category theory are a perfectly natural way to think of type constructors. What I missed in John's interview was any sense of a similar match between categorical structure and structure in the world's many problems. In physics there are certainly some applications with a similar direct correspondence. The Abramsky-Coecke group at Oxford, clearly influenced by the computer science, took categorical ideas of quantum computation which then spilled over into more general foundational ideas. But we can see another principle in play that's more profound that simply saying "types are objects, functions are morphisms". Category theory abstracts away from the internal structure of objects. This is in stark contrast with set-theoretical foundations, which tend to say "everything is a set, so just say which set you are using". Category theory instead stresses how objects interact with each other, using universal characterizations. Computer science takes this as a practical necessity. We don't want to know the "implementation dependent" internal structure of a type or function. That's both impractical and useless, as well as institutionalizing bugs so they become difficult to correct. What we need is the "Application Programmer Interface" (API) of how we can use them. As long as the API is stable, we don't mind if the implementation is changed to fix bugs or make it more efficient. The idea of API matches universal properties in category theory. For the Oxford group, the programmers' "types are objects, functions are morphisms" mutates into the questions like "How do we really use finite dimensional Hilbert spaces?", with the answer expressed categorically. This engineering approach applies to mathematics too. Grothendieck's discovery of toposes came out of a categorical analysis of sheaves. Instead of asking what a sheaf is, you ask how they interact with each other, how we use them. In particular, how do we get sheaf cohomology and other topological invariants out of them? Then it doesn't matter what sheaves are, as long as the category of them has the right properties. I think some of this is part of - to take as an example someone I know - Chris Isham's interest in categories. The scandal of physics is the incompatibility of general relativity and quantum physics, but in both cases it is hard to modify the mathematical structures used without breaking them. It therefore becomes important to ask how we actually use the structures, what is their API, and the hope is that category theory can help. So, to return to John Baez's interview, how might we look for category theory helping to understand the world's problems? We must first look for objects and morphisms, with identities and associative composition, so what are the real-world prototypes of what we are trying to do there? What is the first step beyond the vague aspirations? Steve Vickers
On 12 Aug 2019, at 01:03, Vaughan Pratt <pratt@cs.stanford.edu> wrote:
Formulating the *future *with category theory? My understanding is that the *present *is already formulated less with set theory than with category theory, at least its morphisms under composition, and has been for a long time.
In 1969 Jack Schwartz introduced the programming language SETL based on set theory. However programmers found it much easier to write programs as functions composed from simpler functions than to implement them with sets based on membership, and SETL never caught on.
There have also been sporadic attempts to introduce set theory into K-12 mathematics, under such rubrics as "New maths", starting with the operations of union and intersection, but these have not caught on either.
Category theory is an abstract formulation of functions taking composition as the primitive operation. Functions are in wide use in both mathematics and software. Whenever a function calls another function from within it, that's composition.
In recent years I've been promoting a viewpoint of algebra that emphasizes the associativity of composition as the root of not just algebra but bialgebra in the sense of typed Chu spaces. The defining properties of both homomorphisms and Chu transforms follow from associativity. My most recent talk on this was at FMCS in June, the "ten" slides are here <http://boole.stanford.edu/pub/fmcs.pdf>. (They're less cryptic when the speaker is there to explain them, especially with an audience of only one or two and with no time pressure.)
One might call this "category light" by virtue of working in the *class* CAT, i.e. just categories, no functors etc. By Yoneda (unintended pun there, it's actually "biYoneda") the functors are there, they're just "under the hood". Just as you only need to know what sort of engine is in the car you're driving if you have to service it, you only need to know about functors, natural transformations, etc. when you become a "category mechanic" so to speak.
Sets are automatic because they arise wherever morphisms gather together in those spaces we call homsets.
Vaughan
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]