10
$\begingroup$

(I'm familiar with the lambda-calculus, less so with its categorical models.)

It is well-known that cartesian-closed categories are in tight correspondence to the simply-typed lambda-calculus with function types $A \to B$ and product types $A \times B$. But there are several ways to make this precise -- to build a cartesian-closed category out of the syntax of lambda-terms that is reasonably simple and, hopefully, initial among all CCCs. The construction which I believe is "standard" is to take objects to be contexts $\Gamma$, and morphisms to be simultaneous substitutions $\Gamma \vdash \sigma : \Delta$, where $\sigma$ is a vector of terms, one at each of the types in $\Delta$, using free variables from $\Gamma$.

$$\Gamma ::= \emptyset \mid x:A \mid \Gamma_1, \Gamma_2 \qquad \sigma ::= \emptyset \mid [t/x] \mid \sigma_1, \sigma_2$$

$$\Gamma \vdash \emptyset : \emptyset \qquad \dfrac{\Gamma \vdash t : A}{\Gamma \vdash [t/x] : x:A} \qquad \dfrac{\Gamma \vdash \sigma_1 : \Gamma_1 \quad \Gamma \vdash \sigma_2 : \Gamma_2}{\Gamma \vdash \sigma_1, \sigma_2 : \Gamma_1, \Gamma_2}$$

My question: what is the corresponding "standard" syntactic construction for bicartesian closed categories, that also have sums $A + B$. This is an elementary question, but I have not seen such a presentation worked out. I can suggest one, but it is a bit weird and I wonder if there is a standard one to use instead.

If we want to extend the idea of defining objects as contexts $\Gamma$, we have to decide how to define the formal sum of two contexts $\Gamma_1 + \Gamma_2$. A natural (but somewhat weird-looking) idea is to extend the syntax of explicit substitutions with a formal sum

$$\dfrac{\Gamma_1 \vdash \sigma_1 : \Gamma \quad \Gamma_2 \vdash \sigma_2 : \Gamma}{\Gamma_1 + \Gamma_2 \vdash (\sigma_1 + \sigma_2) : \Gamma} \qquad \dfrac{\Gamma \vdash \sigma : \Gamma_i}{\Gamma \vdash \mathsf{inj}_i(\sigma) : (\Gamma_1 + \Gamma_2)}$$

but the fact that I have never seen this construction anywhere is giving me pause. Do people do it this way, or in some other way?

Here is what I found in the literature:

  • Balat, Di Cosmo, Fiore, 2004: a syntactic model in bicartesian closed categories where objects are simple types, and morphisms are terms with exactly one free variable. This looks reasonably canonical, but also painful to deal with in practice -- I suppose this is why the standard presentation in the cartesian case uses context?
  • More advanced works on sum types use Grotendieck topologies / Sheaves, to build more "precise" models of normal forms. For now I'm rather looking for the simple syntactic models in the simply-typed case.
  • There is a (recent ?) trend to use multi-categories to represent judgments of the form $\Gamma \vdash t : A$, so that we don't have to choose between "objects are types" and "objects are contexts" (objects are types, but the source of a morphism is a context). Is this what people would consider the standard or recommended approach today?
Improve this question
$\endgroup$
10
  • $\begingroup$ You can continue to take the objects to be contexts, but you don't need to consider "sums of contexts". Contexts are still lists of types. The category will have finite coproducts, because every context $x_1 : A_1, \ldots, x_n : A_n$ is isomorphic to a context $x : A_1 \times \cdots \times A_n$, and you can take the coproduct of this type with another. $\endgroup$
    – varkor
    Jun 17, 2021 at 16:15
  • $\begingroup$ $x : (A_1 \times \dots \times A_n)$ corresponds to the one-free-variable presentation. Your suggestion, if I understand correctly, is to hop from the one-free-variable to context presentations depending on what is more convenient (they are isomorphic). But I'm not sure how to do this rigorously in practice. Do you have a pointer to a document that builds a syntactic model in this style? $\endgroup$
    – gasche
    Jun 17, 2021 at 16:27
  • $\begingroup$ To be precise, you would show that the coproduct of $x_1 : A_1, \ldots, x_n : A_n$ and $y_1 : B_1, \ldots, y_m : B_m$ is the context $z : (A_1 \times \cdots \times A_n) + (B_1 \times \cdots \times B_m)$. "Hopping between the presentations" would just be the intuition to guide you into proving the category has the right properties. So really the gist is that the "contexts are objects" approach produces an isomorphic category to the "types are objects" approach. Unfortunately, I don't know of a reference in the literature to this approach, but it's easy enough to check this works yourself. $\endgroup$
    – varkor
    Jun 17, 2021 at 16:51
  • $\begingroup$ @vakor, please post your comment as an answer, I think it's useful. Just one nitpick: the contexts-are-objecs typically produces an equivalent category, not an isomorphic one. $\endgroup$
    – Andrej Bauer
    Jun 19, 2021 at 7:27
  • 1
    $\begingroup$ I believe that Bart Jacob describes an appropiate type theory in chapter 2 of their book Categorical logic and type theory. $\endgroup$
    – Nico
    May 23, 2022 at 14:50

0

Reset to default

Your Answer

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