# Category of Judgements?

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.

-
I do not have the answer but the following paper defines typing judgment on page 38: andrew.cmu.edu/user/awodey/catlog/notes/notes2.pdf –  Mahmud Sep 12 '12 at 0:55
There seem to be two reasonable ways of solving the problem if you restrict the kinds of judgements you're interested in. If you only work with judgements of the form $\phi \text{ true}$ for propositions $\phi$, then you can look at the Grothendieck construction applied to the (pseudo)functor $\Gamma \mapsto \textrm{Sub}(\Gamma) : \textbf{Con} \to \textbf{Cat}$; on the other hand, if you only work with typing judgements, then you can look at the Grothendieck construction applied to the pseudofunctor $\Gamma \mapsto (\textbf{Con} \downarrow \Gamma)$. –  Zhen Lin Sep 12 '12 at 12:02
Why do you expect there to be a category of judgments? –  Mike Shulman Sep 12 '12 at 19:28
@Mike: because categories are pervasive, and whenever a natural object does not form a category, you learn something from that failure. Conversely, if it is a category, you might also learn something from the structure of the arrows (like I did with respect to contexts). Plus it seems that I may have found the answer on other pages of the bLab: it has a comma category structure, related to display maps. Still working out the details. –  Jacques Carette Sep 12 '12 at 21:03
Well, sometimes things only form a degenerate sort of category called a "set". But perhaps you are looking for something like the total category in a fibration that is a ncatlab.org/nlab/show/categorical+model+of+dependent+types ? –  Mike Shulman Sep 12 '12 at 22:30

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", LICS 1987. I think Neil Ghani's work is also relevant. See his PhD thesis, but he will be able to provide better references if you contact him.

-
Thanks, I think that is what I was looking for. I'll need to think about it some more. –  Jacques Carette Oct 5 '12 at 17:57