# Interpreting Minimal STLC using a $\lambda 1$ Category

On page 139, example 2.4.5 of "Categorical Logic and Type Theory" by Bart Jacobs demonstrates the interpretation of the abstraction typing rule with respect to a $$\lambda 1$$ category. Specifically, the category in question is $$(\mathcal C \ell 1 (\Sigma), T_1)$$:

An object of $$(\mathcal C \ell 1 (\Sigma), T_1)$$ is a pair $$(\Gamma,\tau)$$ where

$$\bullet$$ $$\Gamma$$ is a typing context
$$\bullet$$ $$\tau$$ is a type, formed from the types of signature $$\Sigma$$ and the exponent type constructor.

An arrow from $$(x_1:\tau_1 \ldots x_n:\tau_n,\tau)$$ to $$(y_1 : \sigma_1 \ldots y_m : \sigma_m,\sigma)$$ is a pair $$([M_1]\ldots[M_m], [M])$$ where $$M_i$$ is an equivalence class w.r.t. $$\beta$$ and $$\eta$$ of the term-in-context $$x_1 : \tau_1 \ldots x_n : \tau_n \vdash M_i : \sigma_i$$, and $$M$$ is the equivalence class of the term in context $$x_1 : \tau_1 \ldots x_n : \tau_n, x:\tau \vdash M : \sigma$$.

The abstraction rule is interpreted using the right adjoint to the substitution functor induced by the base category's projection arrow $$\pi_{(x_1:\tau_1,\ldots,x_{n-1}),x_n:\tau_n} : (x_1:\tau_1,\ldots,x_{n}:\tau_{n}) \to (x_1:\tau_1,\ldots,x_{n-1}:\tau_{n-1})$$

This right adjoint brings us from the fibre over $$(x_1:\tau_1,\ldots,x_{n}:\tau_n)$$ to the fibre over $$(x_1:\tau_1,\ldots,x_{n-1}:\tau_{n-1})$$.

This works when there are at least two variables in context, but what I would like to know is this: how can we interpret the formation of an abstraction from a typing judgment with a single-variable context? If the base signature contains a nullary symbol, we could use that to silently insert a throw-away type into the "type" position and move the single variable into the "context" position. Is this why the CT structure is required to be non-trivial? That seems kind of awkward, and I'm wondering why it isn't explained in the text.