Suppose that we wanted to construct a mathematical universe where all objects were computable in some sense. How would we do it? Well, we could certainly allow the set \mathbb{N} into our universe: natural numbers are the most basic computational objects there are. (Notation: I’ll use N to refer to \mathbb{N} when we’re considering it as part of the universe we’ll building, and just \mathbb{N} when we’re talking about the set of natural numbers in the “real” world.) What should we take as our set of functions N^N from N to N? Since we want to admit only computable things, we should let N^N be the set of computable functions from \mathbb{N} to \mathbb{N}, which we can represent non-uniquely by their indices (i.e., by the programs which compute them).
An introduction to 2-categories is given by illustrating how the structure of typed lambda calculus may naturally be viewed as a 2-category. In this vein. the structure of computations or conversions gives rise to notions of lax 2':"adjointness.
John Baez Algebraic Topological Methods in Computer Science 2008, University of Paris Diderot (Paris 7) July 7, 2008 Computation and the Periodic Table By now there is an extensive network of interlocking analogies between physics, topology, logic and computer science, which can be seen most easily by comparing the roles that symmetric monoidal closed categories play in each subject. However, symmetric monoidal categories are just the n = 1, k = 3 entry of a hypothesized "periodic table" of k-tuply monoidal n-categories. This raises the question of how these analogies extend. We present some thoughts on this question, focusing on how symmetric monoidal closed 2-categories might let us understand the lambda calculus more deeply. This is based on work in progress with Mike Stay. Click on this to see the transparencies of the talk: