You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Amar Hadzihasanovic (Feb 11 2021 at 13:36):I like the opening to George M. Bergman's 1978 paper, The diamond lemma for ring theory:
The main results in this paper are trivial. But what is trivial when described in the abstract can be far from clear in the context of a complicated situation where it is needed.
It's in a paper on algebra but I think it captures some of the culture of CT.
Fawzi Hreiki (Feb 11 2021 at 14:04):Amar Hadzihasanovic said:
It's in a paper on algebra but I think it captures some of the culture of CT.
Well category theory is algebra - namely, the algebra of composition.
Mike Shulman (Feb 11 2021 at 14:07):Reminds me of Peter Freyd's famous remark that "perhaps the purpose of categorical algebra is to make that which is trivial, trivially trivial."
Fawzi Hreiki (Feb 11 2021 at 14:11):It can be a bit misleading though for that to be viewed as the sole purpose of category theory (not that the quote says that). I think, and I imagine many here do too, that category theory has its own internal aesthetic which is worth studying in the same way that group theory or algebraic geometry is worth studying.
Mike Shulman (Feb 11 2021 at 16:38):Yes, there are many misleading things about that quote. Peter May once suggested that it might be better to say "to make that which is formal, formally formal", since something can be formal without being trivial.
Nathanael Arkor (Feb 11 2021 at 16:39):Perhaps "that which is trivial, formally trivial" also captures the intent better.
Nathanael Arkor (Feb 11 2021 at 16:40):But it's less amusing that way.
John Baez (Feb 11 2021 at 16:49):Mike Shulman said:
Reminds me of Peter Freyd's famous remark that "perhaps the purpose of categorical algebra is to make that which is trivial, trivially trivial."
Reminds me of how when I told Timothy Gowers this, he said something like "For me it's enough that it be trivial".
Jason Erbele (Feb 11 2021 at 19:25):Is there an n-trivialty hierarchy like there is an n-category hierarchy? Perhaps "nontrivial" = (-1)-trivial, "trivial" = 0-trivial, "trivially trivial" = 1-trivial…
John Baez (Feb 11 2021 at 19:32):There is such a hierarchy, but it gets nontrivial when we reach inaccessible cardinals.
Jason Erbele (Feb 11 2021 at 19:34):Sorry – can't resist. Going any further than trivially trivial according to my proposed numbering of the hierarchy might be too trivial (2-trivial). :sunglasses:
Todd Trimble (Feb 12 2021 at 01:16):Nathanael Arkor said:
Perhaps "that which is trivial, formally trivial" also captures the intent better.
Wait, are you just pretending not to know May's version? "That which is formal, is formally formal".
Joe Moeller (Feb 12 2021 at 01:18):No, Mike said that right before.
Todd Trimble (Feb 12 2021 at 01:24):So he did.