# Foundation for category theory

Before a little premise:

It's well known that we can internalize the notion of category, functor and natural transformation in any category with enough structure: for instance we can define what an internal category is in every category with pullback, enriched category in monoidal categories (even if to prove most result we require a symmetric closed one) and also che define internal category in every monoidal category in which the tensor product preserve equalizer.

Now, after some study I get that all these theories serve the purpose to internalize some categorical construction in categories rather different than set, and said theories indeed require classical (i.e. $\mathbf{Set}$-based) category theory (indeed they require the definition of monoidal category, category with some limits etcetc.

So for what I get now the problem is that in order to do category theory we need a category with enough structure (like we need $\mathbb Z$ or symmetric and linear group to do some group theory :) ).

Now for all of you we had the patience to read the premise here the question:

There are other foundational theories that seen in a set-theoretic meta theory have as models some (structured) categories, such that in these theories we can define a concept of category and develop all the classical result and construction which can build in classical set based category theory? (even enriched category theory, higher category theory and so on)

I thank in advance for any answer :)

-
One thing to note is that their is not one category theory, their is a multiverse of category theories, at least one for each model of set theory. In other words, "category theory" will look different in different set theories (read set theories as something like models of ZF or some significant fragment thereof). I think what the OP is asking is what else lives in this multiverse of category theories. I have wondered about this myself, but I do not know how to make a precise question out of it. I think some knowledge of logic would help. – Baby Dragon Jan 7 '13 at 20:57
@BabyDragon Yes, but that's like saying that there is one "group theory" for each model of set theory. That is true in a very precise technical sense and yet almost completely irrelevant to mathematical practice. – Zhen Lin Jan 7 '13 at 21:04
@ineff It begins to look to me like you are asking what makes a 2-category look like a 2-category of categories. Some more recent work on this question revolves around ‘Yoneda structures’; see here, for example. – Zhen Lin Jan 7 '13 at 21:07
You might be interested in this: en.wikipedia.org/wiki/Type_theory#Relation_to_category_theory It tells you how to go from category theory to type theory (which is the wrong way around). – Baby Dragon Jan 7 '13 at 21:16
I also found this a few minutes ago. golem.ph.utexas.edu/category/2013/01/… – Baby Dragon Jan 7 '13 at 23:12