<p>(I'm familiar with the lambda-calculus, less so with its categorical models.)</p>
<p>It is well-known that cartesian-closed categories are in tight correspondence to the simply-typed lambda-calculus with function types <span class="math-container">$A \to B$</span> and product types <span class="math-container">$A \times B$</span>. 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 &quot;standard&quot; is to take objects to be contexts <span class="math-container">$\Gamma$</span>, and morphisms to be simultaneous substitutions <span class="math-container">$\Gamma \vdash \sigma : \Delta$</span>, where <span class="math-container">$\sigma$</span> is a vector of terms, one at each of the types in <span class="math-container">$\Delta$</span>, using free variables from <span class="math-container">$\Gamma$</span>.</p>
<p><span class="math-container">$$\Gamma ::= \emptyset \mid x:A \mid \Gamma_1, \Gamma_2 \qquad \sigma ::= \emptyset \mid [t/x] \mid \sigma_1, \sigma_2$$</span></p>
<p><span class="math-container">$$\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}$$</span></p>
<p>My question: what is the corresponding &quot;standard&quot; syntactic construction for <em>bicartesian</em> closed categories, that also have sums <span class="math-container">$A + B$</span>. 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.</p>
<p>If we want to extend the idea of defining objects as contexts <span class="math-container">$\Gamma$</span>, we have to decide how to define the formal sum of two contexts <span class="math-container">$\Gamma_1 + \Gamma_2$</span>. A natural (but somewhat weird-looking) idea is to extend the syntax of explicit substitutions with a formal sum</p>
<p><span class="math-container">$$\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)}$$</span></p>
<p>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?</p>
<p>Here is what I found in the literature:</p>
<ul>
<li><a href="http://www.dicosmo.org/Articles/2004-BalatDiCosmoFiore-Popl.pdf" rel="noreferrer">Balat, Di Cosmo, Fiore, 2004</a>: 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?</li>
<li>More advanced works on sum types use Grotendieck topologies / Sheaves, to build more &quot;precise&quot; models of normal forms. For now I'm rather looking for the simple syntactic models in the simply-typed case.</li>
<li>There is a (recent ?) trend to use multi-categories to represent judgments of the form <span class="math-container">$\Gamma \vdash t : A$</span>, so that we don't have to choose between &quot;objects are types&quot; and &quot;objects are contexts&quot; (objects are types, but the source of a morphism is a context). Is this what people would consider the standard or recommended approach today?</li>
</ul>

CC BY-SA 4.0
2021-06-17T16:15:25.690Z
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.
varkor
CC BY-SA 4.0
2021-06-17T16:27:15.937Z
$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?
gasche
CC BY-SA 4.0
2021-06-17T16:51:44.277Z
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.
varkor
CC BY-SA 4.0
2021-06-19T07:27:09.393Z
@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.
Andrej Bauer
CC BY-SA 4.0
2021-06-19T07:29:50.893Z
@gasche: I think checking that varkor's idea works is just some fairly simple acrobatics in $\lambda$-calculus, isn't it? You will need some $\eta$-laws for sums, I think. But you'll need those no matter what if you want the syntactic category to have coproducts, because the $\eta$-laws are the "uniqueness" part of the universal property.
Andrej Bauer
CC BY-SA 4.0
2021-06-19T12:17:33.630Z
tI'm not worried about the proposed approach not working, my intuition is that it works just as well as the two approaches I sketched in my post (formal sum of contexts, or one-variable morphisms). But I most wanted advice on which presentation was standard, or at least familiar to other people, to reuse the "usual" style. Between varkor's proposal and the one-variable morphism, I think I would prefer the one-variable morphism: it's only slightly more painful syntactically, and easier to explain/justify.
gasche
CC BY-SA 4.0
2021-06-19T12:21:47.107Z
"You will need some η-laws for sums, I think." Yes, terms need beta-eta on sums. At the level of contexts, it may suffice to impose some slightly stricter focusing-like structure on formal sums (whenever the source context is a sum, the substitution must be of the form $\sigma_1 + \sigma_2$, not $\mathsf{inj}_i~\sigma$), if they suffice to get a canonical representation -- it's a simple structure, only at the toplevel, without (context) variables.
gasche
CC BY-SA 4.0
2021-06-19T18:14:28.033Z
I am curious about what you need this thing for.
Andrej Bauer
CC BY-SA 4.0
2021-06-21T05:09:31.010Z
I would like to understand the categorical models with sums, but before jumping into Grothendieck topologies I would like to extend the simply-typed correspondence between STLC and CCCs with sums. I expected this would be a standard exercise, but apparently "standard" it isn't really.
gasche
CC BY-SA 4.0
2022-05-23T14:50:17.013Z
I believe that Bart Jacob describes an appropiate type theory in chapter 2 of their book *Categorical logic and type theory*.
Nico
<pl.programming-languages><lambda-calculus><ct.category-theory>
What is the "standard" lambda-calculus model for bicartesian closed categories?
gasche
# What is the "standard" lambda-calculus model for bicartesian closed categories?

(Asked by: username_0 on 2021-06-17)

(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](http://www.dicosmo.org/Articles/2004-BalatDiCosmoFiore-Popl.pdf): 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?

**Tags:** pl.programming-languages, lambda-calculus, ct.category-theory

> **Comments:**
> **username_1**: 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.  
> **username_0**: $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?  
> **username_1**: 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.  
> **username_2**: @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.  
> **username_2**: @username_0: I think checking that username_1's idea works is just some fairly simple acrobatics in $\lambda$-calculus, isn't it? You will need some $\eta$-laws for sums, I think. But you'll need those no matter what if you want the syntactic category to have coproducts, because the $\eta$-laws are the "uniqueness" part of the universal property.  
> **username_0**: tI'm not worried about the proposed approach not working, my intuition is that it works just as well as the two approaches I sketched in my post (formal sum of contexts, or one-variable morphisms). But I most wanted advice on which presentation was standard, or at least familiar to other people, to reuse the "usual" style. Between username_1's proposal and the one-variable morphism, I think I would prefer the one-variable morphism: it's only slightly more painful syntactically, and easier to explain/justify.  
> **username_0**: "You will need some η-laws for sums, I think." Yes, terms need beta-eta on sums. At the level of contexts, it may suffice to impose some slightly stricter focusing-like structure on formal sums (whenever the source context is a sum, the substitution must be of the form $\sigma_1 + \sigma_2$, not $\mathsf{inj}_i~\sigma$), if they suffice to get a canonical representation -- it's a simple structure, only at the toplevel, without (context) variables.  
> **username_2**: I am curious about what you need this thing for.  
> **username_0**: I would like to understand the categorical models with sums, but before jumping into Grothendieck topologies I would like to extend the simply-typed correspondence between STLC and CCCs with sums. I expected this would be a standard exercise, but apparently "standard" it isn't really.  
> **username_3**: I believe that Bart Jacob describes an appropiate type theory in chapter 2 of their book *Categorical logic and type theory*.  

---

## 0 answers

