How precise is the statement "STLC is the internal language of CCCs"?

I'm studying some basic category theory in the context of type theory and came across the statement "simply typed lambda calculus is the internal language of cartesian closed categories". However terms and substitutions in the internal language of CCCs are the same data type, unlike in (traditional) STLC. Speaking in Agda, we have

π¹ : ∀ {Γ σ} -> Γ × σ ⊢ Γ
π² : ∀ {Γ σ} -> Γ × σ ⊢ σ
_[_] : ∀ {Γ Δ σ} -> Γ ⊢ σ -> Δ ⊢ Γ -> Δ ⊢ σ

where π¹ is supposed to be a substitution constructor and π² and _[_] are supposed to be term constructors.

This additional first-orderness allows to abstract over substitutions, so we can e.g. write (using de Bruijn indices)

I : ∀ {Γ σ} -> Γ ⊢ σ ⇒ σ
I = ƛ var 0

silly : ∀ {Γ Δ σ} -> Γ ⊢ Δ ⇒ σ ⇒ σ
silly = ƛ (I [ var 0 ])

I don't know what silly is, but it doesn't look like a regular lambda term to me.

So is the internal language of CCCs actually more expressive than STLC or am I misunderstanding something?

Cartesian closed categories correspond to the simply typed lambda calculus with products. Your silly function is just $\lambda x.\lambda y.y$. If you want something that directly corresponds to the simply typed lambda calculus without implying products check out this paper by Bart Jacobs: Simply Typed and Untyped Lambda Calculus Revisited.

Let's instantiate your silly term and spell out what it looks like in type theoretic notation.

First, we're using _[_] at type $(\sigma \vdash \tau \Rightarrow \tau) \to (\Gamma\times\sigma\vdash\sigma) \to (\Gamma\times\sigma\vdash\tau\Rightarrow\tau)$. As a rule and placing in the terms, we get:
$$\frac{z : \sigma \vdash \lambda y:\tau.y : \tau\Rightarrow\tau \qquad \Gamma, x:\sigma\vdash x:\sigma}{\Gamma,x:\sigma\vdash (\lambda y:\tau.y)[z\mapsto x]:\tau\Rightarrow\tau}$$
where $M[z\mapsto N]$ means "substitute $N$ for $z$ in term $M$". Of course, substituting for a variable that doesn't occur does nothing. So, in type theory, the above is (often by definition of substitution) equivalent to just $\Gamma,x:\sigma\vdash(\lambda y:\tau.y):\tau\Rightarrow\tau$. (Closely relatedly, weakening is also often transparent in type theory.) We then lambda abstract to get silly.

As a potential further insight, structural rules like $(\lambda y:\tau.M)[x\mapsto N] \equiv (\lambda y:\tau.M[x\mapsto N])$ with $y$ not free in $N$ come from naturality. This particular case comes from naturality of currying (if you spell it out, you'll see how the "$y$ not free in $N$" part is handled).

However, in this case it was a bit of a fluke that this worked out. In general, the second argument to _[_] should be a substitution, i.e. an arrow from contexts to contexts. In this code, a context is effectively represented by a left nested tuple (ending in an empty tuple). So if the second argument to _[_] does not return a left nested tuple, then _[_] will not behave like substitution. For example, the expression var 0 [ var 1 ] does not correspond to $$x:\sigma, y:\sigma \vdash x[x\mapsto y] : \sigma$$ like we might think, but rather to $$x:\sigma\times\sigma, y:\sigma \vdash \mathtt{snd}(x) : \sigma$$
This second interpretation is an artifact of this particular implementation that was exposed by failing to meet the precondition of _[_]. We would get the intended behavior had we written something like var 0 [pair unit (var 1)]. It would be cleaner and closer to typical STLC syntax to have _[_] take a vector of arrows that get tupled together in a left nested manner.

That this confusion between types and contexts is so easy is particular to CCCs. Most categorical semantics have a strict distinction between types and contexts; they live in separate categories. This is true of the semantics in the above mentioned Bart Jacobs paper. However, this conflation of types and contexts in CCCs makes it possible to discuss the categorical semantics without needing to introduce notions like indexed categories or fibrations.

StackExchange Computer Science Q#54872, answer score: 5