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.

  • $\begingroup$ 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 $\endgroup$ – Sniper Clown Sep 12 '12 at 0:55
  • $\begingroup$ 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)$. $\endgroup$ – Zhen Lin Sep 12 '12 at 12:02
  • 1
    $\begingroup$ Why do you expect there to be a category of judgments? $\endgroup$ – Mike Shulman Sep 12 '12 at 19:28
  • $\begingroup$ @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. $\endgroup$ – Jacques Carette Sep 12 '12 at 21:03
  • $\begingroup$ 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 ? $\endgroup$ – 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.

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

Presumably you discovered my book Practical Foundations of Mathematics and wrote your very flattering private email to me after asking this question and then forgot to update it.

Coincidentally, Andrej Bauer commented on substitution as pullback on his blog and I posted a brief description of my construction there.

  • $\begingroup$ Correct. I did not see a 'category of judgements' in your book though? $\endgroup$ – Jacques Carette Oct 5 '12 at 17:57
  • $\begingroup$ Looking at Type Theory through a Categorist's eyes, a Judgement consists of a <b>string</b> of sentences called hypotheses forming the context on the left and a <b>single</b> sentence on the right. These do not compose, as they stand. However, the treatment that is set at length in my book and briefly on Andrej's blog constructs an <b>elementary sketch</b> pretty much directly from the type theory. Its nodes, two species of arrow and five equations are almost verbatim the forms of judgement in the syntax. $\endgroup$ – Paul Taylor Oct 6 '12 at 10:02
  • $\begingroup$ I have since seen this. One particular 'answer' is actually given in exercises 4.34 and 4.35 of your book. Although it is not quite the same. $\endgroup$ – Jacques Carette Nov 2 '12 at 17:54
  • $\begingroup$ Those exercises were motivated by the work that Robert Seely did in his PhD thesis and in the paper that Andrej mentioned. I believe that there is also an equationally weaker way of setting up the 2-dimensional structure along the lines of a Gray category. However, such details have long since been purged from my brain. $\endgroup$ – Paul Taylor Nov 2 '12 at 20:53

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.