Hi,
I have been interested in foundations for a while, especially categories as foundations. I am of the opinion that, as long as we present the theory of categories in SET, we will not be able to give a reasonable justification for categories as a foundation. (that could be a question: does the persistent presentation of the theory of categories in SET preclude it from taking its place as a foundation?)
How else can we present the theory of categories?
What, in your mind, is a foundation anyway? To me, it is a way to express ideas (language with syntax or diagrammatic calculus or other mysterious thing) and have reasoning that we all agree on because it has precise rules.
My next question is about how to present the theory of categories in a linear logic. I am working on a few intuitions about how to have such a thing. First is the intimate link between linear logic, and the geometry of tensor calculus. Second, we normally think of the geometry of tensor calculus as being only about one particular kind of category. However, the basic reasoning in GTC is about planar graphs. Categories are exactly planar graphs with extra data over the edges. Thus, GTC is also a place to reason about categories in general, not just a particular brand of category.
Is it possible to present the theory of categories in a linear logic and would this presentation not be more of a diagrammatic presentation? GTC comes with a calculational tool. It is a diagrammatic calculus.
Swapping morphisms for arrows in categorical diagrams was a huge turning point for physics: See Markopolou and also see Panangaden, Blut, Ivanov and see Coecke,Abramsky. This swap opened up the diagrammatic calculus. Maybe we should feed this simple change back to category theory as a means of making it more of a foundation.