(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?