Is there any Category Theory tutorial that illustates that we need this apparatus to solve some real problem? For example, for Group Theory there is an excellent book 'Abel's theorem in problems and solutions' that does exactly that.
I think your question is wrong in a sense. Category theory is one of several languagues of mathematics, and there are analogies between them. It's kinda like asking "is there a computer program that requires to be written in C?"
So I think there is an element of taste whether you prefer category theory to some other (logical) language. That being said, just like in programming, it's still useful to know more than one language, because they potentially have different strengths.
Group theory -> Abel's theorem
Category theory -> ???
(below I got the answer 'Weil conjectures')
"For any scheme X the category Et(X) is the category of all étale morphisms from a scheme to X. It is an analogue of the category of open subsets of a topological space, and its objects can be thought of informally as "étale open subsets" of X. The intersection of two open sets of a topological space corresponds to the pullback of two étale maps to X. There is a rather minor set-theoretical problem here, since Et(X) is a "large" category: its objects do not form a set."
There's a lot of advanced math in that paragraph, but it should be clear that Category Theory is needed to define etale cohomology.
This might not meet your criterion exactly, as one can extract a more topological proof and relegate the category theory to a non-essential role, but this requires some more effort and is a harder proof. So I do think it still illustrates that the category theoretic approach does add something beyond just a common language.
Grothendieck wrote modern Algebraic Geometry in the language of Category Theory. This is the first time I saw Category Theory really used in a useful way. Grothendieck's proofs of the Weil conjectures I would say is a good example of using Category Theory to solve a famous problem. Category Theory is used to define and work with etale cohomology and etale cohomology plays a fundamental role in Grothendieck's proofs of the Weil conjectures.
Last years SoME3 has this entrant https://youtu.be/Njx2ed8RGis?si=-Q0TwT8LKmTC9o0R
Also Oliver lugg has a hilarious overview of the topic
That's not an application of category theory. The important theorem here is that the fundamental group is a functor, plus computations of the fundamental group of the disc and the circle. But that's a theorem from topology, not a theorem from category theory. Category theory is merely used as a language, to give the proof a structure.
By that I don't want to say category theory is useless. But regarding the video it's neither necessary, nor an application of category theory.
> Proceed to link to a non-constructive proof
Why are mathematicians like this?
[1]: https://www.youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI...
That said, two comments:
1) The definition of a category is just objects, arrows, and composition. If you're looking for more features, you might be disappointed. (If you've grown up with 'methods' rather than arrows, then you don't necessarily have composition.)
Writing your logic with objects and arrows is just damn pleasant. If I have bytes, and an arrow from bytes to JSON, then I have JSON. If I have also have an arrow from JSON to a particular entry in the JSON, then by the property of composition, I have an arrow from bytes to that entry in the JSON.
2) The various CT structures are re-used over and over and over again, in wildly different contexts. I just read about 'logict' on another post. If you follow the link [2] and look under the 'Instances' heading, you can see it implements the usual CT suspects: Functor, Applicative, Monad, Monoid, etc. So I already know how to drive this unfamiliar technology. A few days ago I read about 'Omega' on yet another post - same deal [3]. What else? Parsers [4], Streaming IO [5], Generators in property-based-testing [6], Effect systems [7] (yet another thing I saw just the other day on another post), ACID-transactions [8] (if in-memory transactions can count as 'Durable'. You don't get stale reads in any case).
They're also widespread in other languages: Famously LINQ in C#. Java 8 Streams, Optionals, CompletableFutures, RX/Observables. However these are more monad-like or monad-inspired rather than literally implementing the Monad interface. So you still understand them and know how to drive them even if you don't know all the implementation details.
However what's lacking (compared to Haskell) is the library code targeting monads. For example, I am always lacking something in Java Futures which should be right there: an arrow I can use to get from List<Future<T>> to Future<List<T>>. In Haskell that code ('sequence') would belong to List (in this case 'Traversable' [9]), not Future, as it can target any Monad. This saves on an n*m implementation problem: i.e. List and logict don't need to know about each other, vector and Omega don't need to know about each other, etc.
[1] https://www.youtube.com/playlist?list=PLCTMeyjMKRkqTM2-9HXH81tvpdROs-nz3
[2] https://hackage.haskell.org/package/logict-0.8.1.0/docs/Control-Monad-Logic.html#g:2
[3] https://hackage.haskell.org/package/control-monad-omega-0.3.2/docs/Control-Monad-Omega.html
[4] https://hackage.haskell.org/package/parsec-3.1.17.0/docs/Text-Parsec.html#t:ParsecT
[5] https://hackage.haskell.org/package/conduit-1.3.5/docs/Data-Conduit.html#g:1
[6] https://hackage.haskell.org/package/QuickCheck-2.15.0.1/docs/Test-QuickCheck-Gen.html#g:1
[7] https://hackage.haskell.org/package/bluefin-0.0.6.1/docs/Bluefin-Eff.html#g:1
[8] https://hackage.haskell.org/package/stm-2.5.3.1/docs/Control-Monad-STM.html
[9] https://hackage.haskell.org/package/base-4.20.0.1/docs/Data-Traversable.html#t:Traversable var tasks = names.Select(GetThingAsync); // IEnumerable<Task<Thing>>
var things = Task.WhenAll(tasks); // Task<Thing[]>, await to get Thing[]
As in, from outside, it looks like you are in there way deep, but it might need some more work to go and fetch the (assumed) target audience.