I have been able to find a lot of information on the **category of contexts** -- for example, the page on syntactic categories at the nLab is a good starting point. However, when I try to find similar information on the **category of judgements**, I find a whole lot less. My guess would be that I am simply not looking for the right term.

To be more specific, I am looking for a reference which defines the **category of judgements** with $\Gamma \vdash t:T$, i.e. term $t$ has type $T$ in context $\Gamma$ as objects, and ???? as arrows (i.e. that is one of the things I am looking for). I am guessing that the morphisms are likely the same as in the category of contexts, namely the substitutions that respect the underlying type theory.

Edit: on top of Andrej's answer, and Paul's book there is also relevant work by Garner such as the paper Two dimensional models of type theory, and the slides Two dimensional locally cartesian closed categories which are quite relevant.

As far as I understand, Seely's work (see links in Andrej's answer) uses explicit reduction paths (based on explicit generators such as $\beta$ reduction) as 2-cells, while the more recent work uses abstract identity types for the same idea. If I understand well, these are essentially the same, just that Seely's work gave explicit generators for the 2-cells, while in homotopy type theory one allows generalizations to higher dimensions, and the simplest way to do this is to let the inhabitants be implicit.

Surprisingly, no one mentionned that the category of judgements is mostly easily seen as the slice category of the category of contexts over a single variable -- as explained over at the n-lab.

typing judgmenton page 38: andrew.cmu.edu/user/awodey/catlog/notes/notes2.pdf $\endgroup$3more comments