Do we need the product type in simply typed lambda calculus for proving that its type category is CCC?

Question

I was reading wikipage about the simply typed lambda calculus and it says about categorical semantics that:

To make the correspondence clear, a type constructor for the Cartesian product is typically added to the above.

But I got confused with the "typically". It seems to me that we would need to add products to it, or else how the type category associated to it would have products? But then the correspondence would be between simply lambda calculus with products and CCCs, and that is not how is stated in the wiki page.

So, do we need the product type in simply typed lambda calculus for proving that its type category is CCC?

Answer 1

There is, in fact, a correspondence between simply typed lambda calculus without a product type and Cartesian closed categories. However, it requires being a bit less naive about how things are set up than is typical for simple explanations. The way it works is as follows...

1. Objects of the category are not just types, but contexts that would be suitable for a typing judgment $Γ ⊢ e : T$. If we agree to use something like de Bruijn notation, then these contexts can just be lists of types.

2. Arrows $Γ ⇒ Δ$ consist of, for each type in $Δ$, a term of that type in context $Γ$. This is the data needed to simultaneously substitute into a well-formed term in context $Δ$ to get a term in context $Γ$.

3. The identity $Γ ⇒ Γ$ is just made up of variables. E.G. $x:A,\ y:B,\ z:C ⊢ x:A,\ y:B,\ z:C$

4. Composition is by substitution. If we have a list $Γ ⊢ Δ$ and a list $Δ ⊢ Σ$, then we can substitute the former into the terms in the latter to get a new list $Γ ⊢ Σ$. That this is associative and unital (under #3) are standard theorems about substitution.

Under this methodology, the category of contexts of STLC without product types is a CCC, and forms a free CCC generated by objects corresponding to any base types in the lambda calculus. And there is a pretty direct correspondence between structure of the lambda calculus and defining structure of the category:

1. Base types correspond to generating objects of the category.
2. Contexts, as finite lists of types, correspond to finite products. Associativity and identity of products corresponds to the flatness of contexts, because the exact nesting structure doesn't matter up to isomorphism.
3. Function types correspond to exponential objects

All of this must be, 'up to isomorphism,' of course, because in a CCC, we are permitted to form e.g. $C^{A×B}$, which does not directly make sense in terms of the described types/contexts. However, it is isomorphic to $(C^B)^A$ which does (assuming $C$ directly corresponds to a type). Also, $(B×C)^A$ is not a type, but it is isomorphic to the context object $B^A × C^A$ provided $B$ and $C$ correspond to types.

If you do include product types, then you can (to some degree) get away with conflating contexts and product types, and terms-in-a-context with functions. And this is what people do when introducing the idea to relative beginners, because it's simpler. However, detailed categorical studies of type theory tend to keep the distinction. This can allow, for example, 'product types' which are not actually categorical products, because the eta rule ($(π_1 p, π_2 p) = p$) is only provable up to some equality type, not an actual calculation rule (the latter is usually taken to coincide with equality of arrows). In cases like this, the context structure can still form a CCC, but the product types are additional, distinct structure.

This methodology is covered in more detail in e.g. section 3 of Normalization and the Yoneda Embedding. It can also be teased out of e.g. Jacobs' Categorical Logic and Type Theory, but I think it's not spelled out quite as explicitly (and the book might be harder to get a hold of).

Answer 2

I believe the Wikipedia author is slightly confused (for further evidence, they seem further down not to realize that every topos is Cartesian closed). Certainly not every simply typed lambda calculus has a Cartesian closed category of types, since for instance any closed monoidal category whatsoever has a simply typed lambda calculus for its internal logic.

Possibly the actual intended result is that it’s possible to include axioms on a simply typed lambda calculus which imply its category of types is Cartesian closed without adding a product constructor explicitly. Intuitively, this should involve transposing all the data in a Cartesian closed category that involves the product across the product–hom adjunction. It’s not clear that any complete reference exists for this process on the categorical side, though, since categorists hardly ever work in closed categories without an adjoint monoidal structure. See here for the idea, with the observation that no reference seems extant: https://ncatlab.org/nlab/show/closed+category#symmetric_and_cartesian_versions