The Cube Equation holds in lambda calculus, with the natural notion of residuals that is present there. It also holds in categories with pushouts, as Barendregt expressed as an Exercise in his 1984 book, and which was around that time proved in detail by Plotkin in a twelve page unpublished hand-written note. Mellies and van Oostrom have taken the Cube Equation and the residual notion as point of departure for the development of a substantial theory of residual systems and axiomatic rewriting theory. There it is shown that the Cube Equation is the key unlocking congruence and confluence properties for braids and other related structures such as Garside monoids. The latter area was explored by Dehornoy and coauthors, as witnessed by their encyclopedic treatise on Garside theory. That enterprise also starts in an (initial) framework of categories with presentations.
QUESTION. In view of the above, one would expect in category theory and higher category theory concerning infinite categories that the Cube Equation and its consequences would be very much present there. Or at least, on occasion present. But it seems that the contrary is the case: nowhere in basic or advanced books on category theory one encounters the Cube Equation, or residual notions. (I would love to be corrected!) How come? Is this because the lambda calculus and rewriting people only deal with syntactical matters, whereas higher category theory such as invoked in Hylands paper with a new view on lambda calculus, are quite something else? Andrew Polonsky in private communication refers to it a few days ago: “Classical Lambda Calculus in the Modern Dress”, https://arxiv.org/abs/1211.5762
Do such syntactical matters as the habitat of the Cube Equation never make an entrance, have an influence, in category theory? Is it so disjoint? Is a fundamental notion as confluence a total stranger in categories? Curious. Is this why people like me experience(d) such a steep learning curve regarding the wonderful and intriguing abstractions of category theory?
Todo: Ask Henk, Gordon, Martin Hyland, Andrew, Roy, Joerg, Pierre Louis, Jean-Jacques, Gerard, Paul-Andre, Vincent, in due time. Or Eugenia Cheng, Emily Riehl, whose informal or introductory books on advanced category theory I’m much enjoying. Curious about comments!
Jan Willem
