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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.