# reperiendi

## PhD

Posted in Uncategorized by Mike Stay on 2008 October 10

I’ll be categorifying the lambda calculus.  The nicest way of doing this would be to develop a good notion of a 2-theory, of which “the theory of a cartesian closed category” would be one example.  It’s already known how to do this for cartesian categories: the kind of 2-theory has products itself, and has one type, $C;$ a morphism $C \times C \to C$ for the product in C and a morphism $I \to C$ for the unit; and several 2-morphisms for the diagrams.

Closed categories, however, need some notion of “op,” which is contravariant.  Figuring out the nicest way of doing this will be some fun research.  Paul Mellies has some ideas.

Hopefully, this kind of 2-theory will also let me talk about things like the blue calculus or Tyler Close’s web calculus (where objects are web services and POST is method invocation; lambda terms are stateless objects responding to the unique “call” method) that he uses in waterken.