Category theoretical proofs always follows the pattern: nothing happens, nothing happens, nothing happens, then an interesting problem is solved.
This really is the elegance of category theory: it is able to express a hard solution problem in seemingly trivial steps.
However, I feel this really illustrate some of the failure of communication for category theory:
- Many attempts simply stop before the "solved a problem" step. The learner often just see a slightly different encoding of an existing problem, and feels "don't know what to do with it", even when the encoding seems general.
- Many attempts seek to solve a problem that the learner is not interested in. If people don't get experience with the hard problem first, then it is hard to feel the categorical proofs.
- Finally, I don't feel "category theory without proof" is a good approach. In my naive view, I still feel category theory is a powerful vessel for elegant proofs, but does not offer much insight in encoding: categorical encoding often feels no different from their elementary counterpart. This property is valuable in proofs, as we can go from a very light encoding into deep theorems really fast, but it is an unnecessary cognitive burden for people who don't need to do proofs.
Cheng Zhang
npub1uc…8q6qy
2026-06-18 12:22:24 UTC
Author Public Key
npub1ucfl35l5pyknn8j3yhghqjljmllxsmmtjggkuxfpu782nnrfj0wqd8q6qyPublished at
2026-06-18 12:22:24 UTCEvent JSON
{
"id": "98104ff86206838bbecb22b8841a68eca0767bc640c52a487a1edd0f8736ca4a",
"pubkey": "e613f8d3f4092d399e5125d1704bf2dffe686f6b92116e1921e78ea9cc6993dc",
"created_at": 1781785344,
"kind": 1,
"tags": [
[
"proxy",
"https://mathstodon.xyz/@czhang03/116771084308684586",
"web"
],
[
"proxy",
"https://mathstodon.xyz/users/czhang03/statuses/116771084308684586",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://mathstodon.xyz/users/czhang03/statuses/116771084308684586",
"pink.momostr"
],
[
"-"
]
],
"content": "Category theoretical proofs always follows the pattern: nothing happens, nothing happens, nothing happens, then an interesting problem is solved.\nThis really is the elegance of category theory: it is able to express a hard solution problem in seemingly trivial steps. \n\nHowever, I feel this really illustrate some of the failure of communication for category theory:\n- Many attempts simply stop before the \"solved a problem\" step. The learner often just see a slightly different encoding of an existing problem, and feels \"don't know what to do with it\", even when the encoding seems general.\n- Many attempts seek to solve a problem that the learner is not interested in. If people don't get experience with the hard problem first, then it is hard to feel the categorical proofs.\n- Finally, I don't feel \"category theory without proof\" is a good approach. In my naive view, I still feel category theory is a powerful vessel for elegant proofs, but does not offer much insight in encoding: categorical encoding often feels no different from their elementary counterpart. This property is valuable in proofs, as we can go from a very light encoding into deep theorems really fast, but it is an unnecessary cognitive burden for people who don't need to do proofs.",
"sig": "03d22b112ceb9acd1bd1a5f83ab870c9d04fd76831595cadaa8561aff4ec6890824539ffd13a748d6365c7098890a72cad0375f5a0a0a0d9f68016e888006cd1"
}