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?