10
$\begingroup$

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.

$\endgroup$
8
  • $\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$ Sep 12, 2012 at 0:55
  • 2
    $\begingroup$ Why do you expect there to be a category of judgments? $\endgroup$ Sep 12, 2012 at 19:28
  • 1
    $\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$ Sep 12, 2012 at 21:03
  • 1
    $\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$ Sep 12, 2012 at 22:30
  • 1
    $\begingroup$ "Categories are pervasive"? Ubiquitous, very useful tools, yes. However, the way that you say this suggests that you are expecting a unique "blinding light" answer. But categories are (just) (useful) tools: you can change them around to do lots of different things. What is really not clear to me from the discussion that I have had with you on this topic in various public and private fora is what information you want the 2-cells to convey $\endgroup$ Nov 2, 2012 at 21:33

2 Answers 2

8
$\begingroup$

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.

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

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.

$\endgroup$
4
  • $\begingroup$ Correct. I did not see a 'category of judgements' in your book though? $\endgroup$ Oct 5, 2012 at 17:57
  • 1
    $\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$ Oct 6, 2012 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$ Nov 2, 2012 at 17:54
  • 1
    $\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$ Nov 2, 2012 at 20:53

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.