In my experience, what computer scientists (in particular programming language researchers) consider to be "category theory" is very different from what mathematicians (in particular those working in algebraic geometry, algebraic topology, homological/homotopical algebra, ...) consider to be the important parts of category theory.

In my very biased and unfair perspective, the "computer science perspective" on category theory is rather applying the first 50 introductory pages of a decent textbook about category theory, while for mathematicians, where category theory actually starts to become somewhat interesting is only, say, from page 150 on, when also a lot of additional mathematical concepts that actually motivate (or even necessitate) these much more complicated category theory topics have additionally become introduced.

But why is that a problem?

Category theory is an API for mathematics that was developed with specific applications in mind that the API seeks to unify and make easier to think about. Those application domains are algebraic geometry, algebraic topology, homological/homotopical algebra. Every API comes with trade-offs: typically an API makes one domain easier, at the cost of making other domains harder. Example: CSS is Turing complete. And I think CSS is really good at helping with styling webpages. But I would not want to write a compiler is CSS.

Computer scientists, like myself, who read from Page 150 onwards have just found the API stylised for algebraic geometry, algebraic topology, homological/homotopical algebra, ... not that useful, for applications in computer science. Unlike the first 50 pages, which have been very useful. More specifically, we found the cost of using purely categorical APIs not worth the benefits in many application domains. Maybe we are missing something, maybe we overlooked something. But, given the investments since the 1990s of computer science into category theory, I'd like to see more evidence for!

To conclude with a concrete example: why would I write a compiler using an API for homotopical algebra?

Who told you that?

Don't think anybody told me that, but I do believe it to be the case

Why?

Category theory is equivalent to type theory.

It's probably more accurate to say that they are complementary rather than equivalent.

- Category theory emphasizes morphisms and composition

- Type theory emphasizes terms and computation

There are important correspondences between them (like the Curry-Howard-Lambek correspondence), but they have different strengths and different ways of expressing concepts.

Sorry, I couldn't resist the temptation of being a pedantic formalist.