# Type theory - category theory correspondence

As explained here, simply typed lambda calculus can be viewed as a syntactic language for category theory. My question is, can the following modification make it equally well a formal syntactic language for 2-category theory?

It goes something like this: we have a universe $$U$$. For each $$X : U$$, we make $$X$$ into the universe of a simply typed lambda calculus by introducing the necessary type formation rules. Maps $$a \rightarrow b$$ for $$a, b : X$$ are like maps of objects, under the usual correspondence.

In this setup, I would expect maps $$X \rightarrow Y$$ for $$X, Y : U$$ to correspond to functors in some way, and I would expect some kind of correspondence between type theories of this kind and $$2$$-categories.

More generally, I expect that introducing a higher universe is like passing from $$n$$-categories to $$n+1$$-categories. For a similar idea, applied instead to homotopy type theory, we might expect to get a model for $$(\infty, 1)$$-categories. Has anyone pursued an approach like this?

• I really like the question, but it is more a research project than a MO question. A few steps in this direction have been made here: arxiv.org/abs/1705.07442. It's hard to say how "definitive" this answer is to the problem of $(\infty,1)$-categories. Another important reference, gathering the state of art up to 1991, is T. Streicher, Semantics of Type Theory: Correctness, Completeness, and Independence Results. Jan 1 '20 at 10:11

For the 2-categorical part there is Robert Seely's paper Modelling computations: 2-categorical framework from LICS 1987, and of course a bunch of papers that came afterwards that cite the paper. As Ivan points out, the $$(\infty, 1)$$-aspects of computation are current research.