Just do it, Jean-Pierre. It will be very interesting to see it.
Generally speaking, we do such things all too little. When we wrote our book on quantales we came across a few such historical pathways, one of which was the monad and e.g. also the star composition of natural transformation. We spent a "reasonable portion of time" unravelling that history, and it comes down to less than one page, so we could have done more. We also had a chapter on finite machines and modules, and we look back on finite machines, where CS fixes the "origin" to some paper or papers, but when we looked at it, these "original papers" were quite sparse in their bibliography, which kind of "boosted their originality".
For a while I've been looking into the categorization of foundations, i.e., not the foundations of category theory. For decades we have had a formal term monad which has shown to be useful for categorization of formulas, entailment, proof rules and proofs, etc. Categorical constructivity is very diametral to the traditional "putting symbols one by one in sequence" approach in logic and foundations, which leads to antinomies and many other strange situations. This work, which is all too much for me personally, and I can do only fractions, involves many historical pathways, e.g. Schröder tp Peano, Peano to Principia; Hilbert's lectures 1917-1922; deduction by Hertz and Post; Bernays; Hilbert's and Ackermann's logic foundations; Gödel 1931 and just before; Hilbert-Bernays Grundlagen 1934/39; Church, Turing, lambda calculus and computing; etc. just to name a few. Category theory existed at that time, because of set theory, even if it wasn't "discovered" just by the end of this "mathematical foundations pathway". So I'm fascinated by the thought that that categories would have been "discovered" already before Principia. Principia said that "logic must be freed from the burden of algebra", and foundations never recovered from that attitude. Bernays and Gödel wrote letters in the early 1960's about "something new called category theory" and "there was a guy speaking about something in Poland" (it was Mac Lane), but they simply thought a bit on foundations of such categories rather than such categories being used in constructions in their foundations, that had puzzled them for almost half a century. My point here is that "tracing far back" is very important. Categorization of foundations (Hilbert wasn't even close, but he could have been) connects subpathways in this history and e.g. makes criticism against antinomies (like e.g. Gödel 1931) quite precise.
So, Jean-Pierre, just do it. Or anyone else thinking similarly about "deep tracing", just do it, because nobody else will, most probably. We need to strengthen the culture of "deep tracing", rather that desperately seeking for "this was the moment, this was the breakfast, these were the persons around that table at that moment in time, and that person must be named as the originator, for that person we must create a bust". "Deep tracing" opens up more research, "creating busts" does the opposite.
Best,
Patrik
I guess it is a paper like this one that justified Eilenberg & Mac Lane's choice of terminology. It would be interesting to trace how far the terminology goes back, who used it and where.
Jean-Pierre
You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files | Leave group | Learn more about Microsoft 365 Groups
| You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. |
| View group files | Leave group | Learn more about Microsoft 365 Groups |