The iceberg metaphor
In his excellent lectures Category Theory for Programers, Bartosz Milewski describes Category Theory as the unifying theory for a few other mathematical theories.
When I was watching this, in my head I pictured something like this:
In this picture I wanted to say that different theories where discovered/invented at different times and one day we found out about Category Theory which unified all previous discoveries.
The Holy Trinity
Then I continued my learning and I came across this lecture about Type Theory.
In this lecture, Robert Harper offers the concept of the Holly Trinity, where Category Theory, Proof Theory and Type Theory all correspond to one another.
In this vision, all three are one viewpoint of the same thing, i.e. they are on the same level of abstraction. And you can indeed have correspondence tables like this one.
So, which one?
Which vision would be the more accurate? Is Category Theory a unifying theory that lives at a higher level of abstraction? Or is it just one side of a dice?
Best Answer
I don't see a reason why both viewpoints (and more) aren't accurate.
From one viewpoint, category theory provides a language for isolating abstract structures arising in a wide variety of areas of mathematics. The category theoretic notion of a 'product', for example, captures the notions of cartesian product of sets, direct sum of vector spaces, conjunction of formulae, greatest common divisor of integers, ...the list goes on. From this perspective, your first viewpoint applies (with more than just set theory, logic and type theory on top of the iceberg).
From another viewpoint, category theory is a setting for the semantics of different systems of logic: cartesian closed categories interpret $\lambda$-calculus, toposes interpret intuitionistic first-order logic, locally cartesian categories (kind of) interpret Martin-Löf dependent type theory, and so on. Categories have internal languages, which are type theories, and type theories have semantics in categories: this aligns more closely with your second picture.
From yet another viewpoint, a category is just a mathematical object built out of a couple of sets with some additional structure satisfying certain axioms, just like groups, rings, vector spaces, and so on. In this sense, category theory is just a branch of algebra which studies the algebraic properties of these algebraic structures that we call 'categories'. In this case, a more accurate picture would just be a small blob inside whatever foundational system you're working inside of.
So what is it? I don't think there is, or has to be, a single answer to your question.