ct.category theory - What are κappa-categories?

The intuitive explanation is that $kappa$-categories are to first-order functions what cartesian closed categories are to higher-order functions.

This all started with Lambek's work on polynomial categories; the best reference for that is
J. Lambek. Functional completeness of cartesian categories. Annals of Mathematical Logic, 6:251–292, 1973. That paper introduced the choice of the letter $kappa$. A polynomial category is what you get when you take a category with a terminal object, pick an object $X$, and then freely adjoin a new morphism $f:1to X$ and close under composition. This is very much like the ring of polynomials $R[X]$ over a ring $R$ arrived at by adjoining an indeterminate element and closing under the ring operations. Lambek shows that this property can be stated in universal terms -- as the unique category admitting a particular kind of functor from the original category. This is formally more satisfying but not the best route for beginners.

Later, Hasegawa developed this idea much further in M. Hasegawa. Decomposing typed lambda calculus into a couple of categorical programming languages. Lecture Notes in Computer Science, 953, 1995. He showed that just as the $lambda$-calculus can be used as a "syntax" for specifying morphisms in a cartesian closed category, so too can the $kappa$-calculus -- roughly the $lambda$-calculus without first-class functions -- be used as a "syntax" for specifying morphisms. I recommend studying the figure immediately after the first paragraph of section 3 in his paper (very carefully). It conveys both the essence of these categories and their relevance to the study of programming languages.

To wrap up, cartesian closed categories have been an immensely useful tool in understanding programming languages with first-class functions. Unfortunately they can only be used to study languages with the property that for every pair of types $B$ and $C$ there is also a type of functions from $BRightarrow C$ and the ways of getting a $BRightarrow C$ from an $A$ are in one-to-one-correspondence with the ways of getting a $C$ from a (cartesian) pair of an $A$ and a $B$. Lambek-Hasegawa $kappa$-categories are an elegant way to extend these techniques to languages in which this assumption does not hold.

Lastly, as a postscript, both Lambek and Hasegawa assume that the underlying monoidal structure of their categories is Cartesian. Some of the most fascinating results arise when you repeat their constructions in categories which are merely binoidal or premonoidal -- you'd be surprised how few modifications are required.

• Next dg.differential geometry - What are CR manifolds like?
• Previous nt.number theory - Uniformly computable classes of graphs