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.



linear logic, diagrammatic calculus and foundations
Just to address one of the issues raised by the questioner: the formal theory of categories does not depend on $Set$, any more than the formal theory ZFC depends on $Set$ (what would the latter even mean?). It's just a first-order theory. One formal syntactic presentation of it can be found [here](http://ncatlab.org/nlab/show/fully+formal+ETCS); there is no mention of $Set$ or "collection" or anything like that. 


Naturally, the conventional mode of presentation involves words like "a category consists of a collection $C\_0$ of objects, and collection $C\_1$ of morphisms", etc., etc. This is usually done at a pre-formal level, and has the advantage of readability. It's a kind of pre-formal semantics where the word "collection" is left unanalyzed. If one goes further, and demands that "collections" be sets which are elements of a structure $(V, \in)$ satisfying some set-theoretic axioms such as ZFC, then ultimately one is giving the notion of an interpretation of the theory of categories in the theory ZFC. But the formal first-order theory of categories, insofar as it is given syntactically, stands perfectly well on its own, as does the theory of ZFC. There is no dependency in either direction. 


(Of course, category theory manifestly refers to set theory wherever it uses words like "small" and "locally small", but this is a different issue.) 


The amount of first-order logic needed to express the theory of categories is small: in the jargon, the data and axioms are "essentially algebraic" (i.e., they can be given in terms of a sequence of operations where the domain of each partially defined operation can be specified in terms of equations involving previous operations). This means that "internal category objects" need very little ambient structure to express them: they can be defined in any category with finite limits. The theory ZFC needs much more first-order logic, and correspondingly much more ambient structure to interpret it internally. 


If you want to beef up the theory of categories to a "foundational theory" which will serve the needs of most mathematicians, one has various options. Among them is ETCS (see the page I liked to above for the formal theory), which is weaker than ZFC but probably suffices for most purposes. 


I am not sure what you mean by giving the theory of categories within linear logic. If you mean multiplicative linear logic, you will have to deal with the axioms that involve the contraction and weakening rules for conjunction, which one doesn't have in MLL. 


Added: as far as diagrammatic presentations are concerned, you might be interested in the Q-sequences of Freyd, as discussed in the book Categories, Allegories. 


