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.
