I have been able to find a lot of information on the **category of contexts** -- for example, the page on [syntactic categories](http://ncatlab.org/nlab/show/syntactic+category) 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](http://www2.math.uu.se/research/pub/Garner5.pdf), and the slides [Two dimensional locally cartesian closed categories](http://web.science.mq.edu.au/~rgarner/Talks/2LCCC.pdf) 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](http://ncatlab.org/nlab/show/categorical+semantics#ContextsAndTypeJudgements).



Category of Judgements?
One way to set up a category is to use contexts as objects, and declare that a morphism from the context $\Gamma = x\_1 : A\_1, \ldots, x\_m : A\_m$ to the context $\Delta = y\_1 : B\_1, \ldots, y\_n : B\_n$ is an $n$-tuple $(t\_1, \ldots, t\_n)$ where $$\Gamma \vdash t\_i : B\_i.$$
Composition is given by substitution. Then a judgment of the form $\Gamma \vdash u : B$ is just a special morphism whose codomain is the context $y\_1 : B$. This sort of thing can be read about in Paul's book.


If you really insist on having judgments as *objects*, rather than morphisms, you could impose a further 2-categorical structure. Say that a 2-cell from $\Gamma \vdash u : B$ to $\Gamma \vdash v : B$ is an *equality* $\Gamma \vdash u = v : B$. What kind of equality you use may depends on what your are doing. This way you will get a groupoid-like structure. You could also use one-way *reductions* as 2-cells, for example $\beta$-reductions, in which case your 2-category will look like a poset enriched category. See the paper by R. Seely,
"[Modelling Computations: A 2-categorical framework](http://www.pps.univ-paris-diderot.fr/~mellies/mpri/mpri-ens/articles/seely-modeling-computations-a-2-categorical-framework.pdf)", LICS 1987. I think Neil Ghani's work is also relevant. See his [PhD thesis](https://personal.cis.strath.ac.uk/neil.ghani/papers/yellowthesis.ps.gz), but he will be able to provide better references if you contact him.


