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?

  • 2
    $\begingroup$ 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. $\endgroup$ Jan 1, 2020 at 10:11

2 Answers 2


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.

  • 1
    $\begingroup$ Is this really what the question is asking though? It's true that Seely uses a 2-categorical framework to model lambda calculus where the 2-cells are reductions. But in most type theories that I know, these reductions are necessarily invertible. In a general 2-category I'm not sure there is a type theory which could be considered an "internal language of a 2-category". $\endgroup$ Jan 3, 2020 at 11:10
  • $\begingroup$ Well, the author accepted my answer :-) $\endgroup$ Jan 3, 2020 at 21:14

Some references to some approachesthat exist in the literature have been given in Andrej's answer and Ivan's comment. A couple others are Licata-Harper's work on two-dimensional directed type theory and Licata-Riley-Shulman's work on fibrational frameworks (specifically the "mode theory" is a 2-dimensional type theory).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.