# Which family of bicartesian closed functors can define the semantics of simply typed lambda calculus with products and sums

Given any bicartesian closed category $$\mathbf{C}$$, any natural number $$n \geq 0$$, and any vector $$\boldsymbol{A} \in \mathbf{C}^n$$ with $$n$$ objects $$A_1, A_2, … A_n \in \mathbf{C}$$, how can I define a bicartesian closed category $$\mathbf{STLC}_n$$ and a bicartesian closed functor $$\operatorname{F}_{\boldsymbol{A}} : \mathbf{STLC}_n \to \mathbf{C}$$ with the following properties?

The objects of $$\mathbf{STLC}_n$$ should be

1. $$0 \in \mathbf{STLC}_n$$ the initial object,
2. $$1 \in \mathbf{STLC}_n$$ the terminal object,
3. $$\alpha_1, \alpha_2, … \alpha_n \in \mathbf{STLC}_n$$ $$n$$ named base objects
4. $$\sigma_1 \in \mathbf{STLC}_n , \sigma_2 \in \mathbf{STLC}_n \implies \sigma_1 + \sigma_2 \in \mathbf{STLC}_n$$ all coproducts
5. $$\sigma_1 \in \mathbf{STLC}_n , \sigma_2 \in \mathbf{STLC}_n \implies \sigma_1 \times \sigma_2 \in \mathbf{STLC}_n$$ all products
6. $$\sigma_1 \in \mathbf{STLC}_n , \sigma_2 \in \mathbf{STLC}_n \implies \sigma_1 \to \sigma_2 \in \mathbf{STLC}_n$$ all exponentials.

The arrows of $$\mathbf{STLC}_n$$ should be “all” (in some non-trivial sense) simply typed lambda calculus terms with base types $$\alpha_i, 1 \le i \le n$$, products and sums. Composition of arrows should be defined so that $$\operatorname{F}_{\boldsymbol{A}}$$ “works”, that is, preserves composition and bicartesian closedness.

Further, for all $$i, 1 \le i \le n$$, $$\operatorname{F}_{\boldsymbol{A}} \alpha_i = A_i$$. Given the mapping of the initial and terminal object, the mapping of all other objects are uniquely determined by the bicartesian closed nature of $$\operatorname{F}_{\boldsymbol{A}}$$.

• What's wrong with taking the fixed-point of what you wrote, as a syntactic category?
– cody
Oct 16, 2023 at 22:33