Approaching Type theory and Category Theory as a starting point in the study of mathematics?

Question

I'm a Computer Engineering student, with interest in Type Theory and Category Theory and i have a more pedagogical/philosophical question about these areas.

It seems that many researchers in Type theory and Category Theory in general, specially in Homotopy Type Theory, see their areas as a good starting point for any student to learn mathematics. Their philosophical focus point seems to be the complete exclusion of set theory in the beginning of mathematical courses, in favor of the constructivist/type theoretical approach.

From what i have already read, this idea seems also good for computer science courses, but it comes at a cost which is the topic of this question: as a non-mathematician, all tries of bridging the gap between beginners, also called by Terrence Tao "the pre-rigorous stage", and these areas seem infertile.

For example: the only real "beginner friendly" book on category theory is, by far, Category Theory for Programmers by Bartosz Milewski. Steve Awodey's book, even if it states that it is "for everyone else", is, intentionally, filled with examples of higher mathematical structures which complicate rather than simplify its content.

And it does not serve as a beginner book for another reason: it does suppose a more advanced mathematical maturity (what Tao might define as a "rigorous stage" maturity), which is, in many places (like Brazil where i live), developed in more set-focused courses like Analysis, Topology, etc.

I have faith in the intent, so my question is more in the terms of: What books would you recommend on Category Theory and Type Theory that makes one go from "pre-rigorous" to "rigorous", i.e. learn how to prove things while learning mathematics like Analysis does, and suppose no background (at all)? Is there such book?

And more: if you were a professor in an introduction to mathematics course and wanted to teach people that came straight out of school what mathematics is all about using only Category Theory and Type Theory, what book would you use?

Answer 1

Disclaimer: The following is subjective, and opinions may, of course, differ.

I don't think it makes sense to try to 'learn mathematics' by learning category theory -- it puts the cart in front of the horse.

There are many angles from which you can arrive at category theory: You may find classical category theory a useful unifying language for basic structures like abelian groups, vector spaces, etc. You may come from a CS standpoint, learning about more and more expressive type systems, pondering about the meaning of equality, and ending up studying HoTT, meeting others who arrived there in search for a synthetic approach to homotopy theory. Or you may dislike that set-theoretic foundations allow you to ask "Is $e\in\pi$?" and consider ETCS as an attractive way out. The list goes on.

All these examples have you end up learning some aspect of category theory (cf. "Sketches of an Elephant"), but they all have in common that category theory answers a question -- throw away the question and it becomes meaningless. For example, what is a freshman supposed to make of the notion of an abelian category if they have not, at least, encountered the concrete examples of, say, vector spaces and abelian groups, first?

I sometimes get the impression that category theory is, with awe, seen by young students as being the 'holy grail' of mathematics. In my mind, it really isn't -- certainly at least as far classical category theory is concerned: Ideas mostly happen in concrete examples, while category theory is extremely valuable (essential in fact, I'd say) in telling generalities from specifics. But, in the words of one of my professors back in the day: "It's not enough to just say 'morph morph' all the time."

As someone who wrote his PhD on (homotopical) category theory and now uses type theoretic logical foundations every day, my advise to young students would be: Do familiarize yourself with, and do enjoy and embrace the generality and conceptual clarity of, the different aspects of category theory, but do this alongside, not instead of, the acquisition of a solid 'classical' mathematical education.

Answer 2

While I haven't succesfully accomplished the task of understanding either subjects to a satisfactory level myself, I can recommend some books which would allow someone sufficiently intelligent to achieve it:

1. Sheaf Theory through examples by Daniel Rosiak

This goes through category theory from view point of philosophy, so it's as pure as you can get. Bonus is that introduces topology from basics too.

2. Eugenia Cheng Joy of Abstraction

This has more or less a high content overlap with the first book, but I found the early sections to be more easy for someone to get what ct is about.

There are also some misc stuff like Tom leister notes and so on which will still aid you. You can also check the catsters on youtube.

---

I haven't found any good resources which go over the typetheory- category theory link from programming prespective other than Bartosz Milewski.

If you are anything like me, you'd probably be lead to studying a bit of Haskell. Perhaps relevant CS SE post

However, I gaurantee you will be dissapointed. Most people who do functional programming don't care/ are totally not in the know of category theory. I also find that something Lambda Calculus is more important in regards to application, and if you spend some more time, you'd find that something even more esoteric can be seen to have foundations for lambda calculus, combinators. Stephen Wolfram had written a book about this, but I found it too annoying to read as it was really an advertisement for the wolfram language in hidden form. There seem to be some youtube videos created on it as a result of SOME, so you can check that out.

But anyways, you can also check out the Homotopy type theory book. The subject matter is different, but the early sections do discuss the essence of type theory (or at least tries too). I found some people I know personally also don't like this book at much so YMMV

The rabbit hole is extraordinarly deep and you'd at some point question if mathematics has any foundations at all... see this reddit post

---

Finally I'd like to remark that whule category theory can capture topological notions well ( see Tai danae Bradley's book), it seems to be low Utility in understanding analysis things with derivatives in it. Personal experience and conversations with some expert has led me to the understanding that the the general methods in ct can't be adapted to explain most of analysis stuff, it requires a lot of specialisation. But, I think there is some effort to bridge the link still, I remember seeing a paper where lebesgue integral is introduced by ct ( altho I never read it myself).

Answer 3

As a physicist who taught themselves the basics of category theory (with help from category theorists), trying to learn mathematics from category theory sounds horrible. I suspect there is an unspoken assumption by those saying you should learn category theory to learn mathematics that you are solidly in the rigorous phase of your education, or you are already starting to become post-rigorous. For context of my skill level, I'm probably somewhere between those levels in mathematics (and post-rigorous in physics which probably allows me to punch above my weight).

However, what I've found in trying to use category theory is that the major advantage is to connect different fields and see how they are similar, and from that you can get post-rigorous intuition by saying both these mathematical structures have similar or the same group theoretic properties, therefore my intuition from one transfers to the other. This could mean a well known proof in category X can be lifted to category Y because they have the same basic tools the proof uses. Or you can see that the proof by X et al is essentially the same as the proof by Y et al. But generally anything you can prove with category theory, you can prove using tools specialised for your particular topic.

There are counter examples to this claim, wherein the use of category theory makes a proof cleaner in ways that aren't obvious in the original framework. The best example is that higher homotopy groups are Abelian is much more elegant by just talking about it as a functor between two categories and assuming a single property of the category basically makes this proof a few lines and easier to believe, while the original proof is several pages long. I'm sure others who know the field can give more examples of where category theory simplifies proofs or proves things unknown previously.

What I have found useful in my everyday life from learning category theory was not the actual tools themselves, but the way of thinking that makes it much more natural for me to abstract things. Though this could also have partially been that I was forced to develop to post-rigorous thought to comprehend what I was trying to teach myself (having been fairly comfortably rigorous when I started learning category theory). As for references, I'd say lectures might be more useful if you wanted to learn category theory, maybe this course which was guided more by engineers for engineers https://applied-compositional-thinking.engineering/ (though was solid for basic stuff and had a category theorist involved). Maybe peruse some of the talks from the applied category theory conference might also be interesting (https://msp.cis.strath.ac.uk/act2022/) but many probably assume a much greater skill level but there were a few about programming (e.g. James Fairbanks as a coauthor) that might give some insights since you are coming from engineering/programing.