# 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?

• This looks like crappy propaganda by people who don't actually understand mathematical foundations. Commented Nov 15, 2017 at 23:10
• Simplistic being the key here. Simplistic analogies are a surefire way to distort, marginalize, and otherwise plant "catchy buzzword ideas" into people who will not remember the actual details later (as history has shown us with Gödel's Incompleteness Theorem). So yes, I am pretty damn annoyed about the use of simplistic analogies. Commented Nov 16, 2017 at 7:28
• And how many people out there know that the atom is not a sphere? (Even of those people who know what an atom is, and think they know what it looks like?) Also, you're not in secondary school anymore. Commented Nov 16, 2017 at 7:44
• And I would not present that silly iceberg model. To say that set theory is just a prong of ice coming out of the underlying category theory is to say "hey, I know absolutely nothing about set theory, but let me still claim something about it!" Commented Nov 16, 2017 at 7:45
• I don't see how my comment says that you should stop trying to learn. If a child comes to class with a homework assignment about Mein Kampf you should tell him it's a crappy Nazi propaganda and not be gentle or coy about it. They made a good movie with that premise. You decided to take my comment to heart as a comment about you, and it wasn't. It was a comment about the first image, and that is what you came up with, it's a comment on your teachers more than a comment about you. Commented Nov 16, 2017 at 8:14

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.

• That's an interesting perspective thank you. I'll keep the question open to get other opinion if there is one, but I'm quite satisfied with your answer. Regarding iceberg yes it was just supposed to be a few examples rather than being exhaustive Commented Nov 15, 2017 at 21:51

In my vision the first image could be a bit "more correct". You could use Set (as in Category of Sets) instead of Set Theory (not all Set operations are categorical - eg. union). Category Theory is just an alternative, a more powerful one to Set Theory. As are Type Theory and Intuitionistic Logic (as method of reasoning). So, the way I see it, starting from the second picture, if you choose Category Theory as your reference and zoom into it to see the representation of the others, the semantics of simply typed lambda calculus, as Clive said, lives in Cartesian Closed Categories among which is the Category Set, as are many other categories.

• Does category theory has the power to show that you need stronger foundational assumptions if you want to assume all sets are Lebesgue measurable? Because if not, I don't see how it is a more powerful foundation. Commented Nov 16, 2017 at 7:53
• I meant powerful as abstract and constructive form of reasoning, not as being a foundation of mathematics. Yes, if we assume axioms, we have theories, be it set theory or homotopy type theory, but then we don't have constructive math. However I think the topic is about Category theory and Type theory and the relation between them, not about foundations of math. As abstract forms of reasoning, we need to accept that there are things which are not provable to be right or wrong, so to say that something is in a set or in its complement, in my view is a too strong statement. Commented Nov 16, 2017 at 12:21
• @AsafKaragila: I think category theorists look at that sort of issue from a completely different perspective -- they don't think "How do you need to modify your foundations so that Set has property X?" but "How do I construct a nice topos for which X holds internally?"
– user14972
Commented Nov 16, 2017 at 18:40