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}}$.

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


Your Answer

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