Foundation for category theory

674 Views Asked by At

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:

Are there 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 constructions 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 :)