一句话：提出 transpension 类型作为 shape 上全称量化的右伴随，并给出类型规则与 presheaf 语义。
依赖类型论的 presheaf 模型广泛用于 HoTT、参数性以及 directed/guarded/nominal 类型论，但已有内部 presheaf 算子（√、extent、Gel、Glue、Weld、mill、strictness axiom 等）表达力关系不清，且 shape 变量常需 affine 使用。本文提出 transpension 类型：它是 shape 上全称量化的右伴随，可视为 HoTT 中 suspension 的依赖版本。作者给出一般类型规则与基于 multiplier（基范畴函子）的 presheaf 语义，其中结构规则取决于 multiplier 特征。结果表明，与 strictness axiom 结合可实现并改进多种内部化算子（locally fresh names 除外，未作形式化断言）。
Presheaf models of dependent type theory have been successfully applied to model HoTT, parametricity, and directed, guarded and nominal type theory. There has been considerable interest in internalizing aspects of these presheaf models, either to make the resulting language more expressive, or in order to carry out further reasoning internally, allowing greater abstraction and sometimes automated verification. While the constructions of presheaf models largely follow a common pattern, approaches towards internalization do not. Throughout the literature, various internal presheaf operators ($\surd$, $\Phi/\mathsf{extent}$, $\Psi/\mathsf{Gel}$, $\mathsf{Glue}$, $\mathsf{Weld}$, $\mathsf{mill}$, the strictness axiom and locally fresh names) can be found and little is known about their relative expressivenes. Moreover, some of these require that variables whose type is a shape (representable presheaf, e.g. an interval) be used affinely. We propose a novel type former, the transpension type, which is right adjoint to universal quantification over a shape. Its structure resembles a dependent version of the suspension type in HoTT. We give general typing rules and a presheaf semantics in terms of base category functors dubbed multipliers. Structural rules for shape variables and certain aspects of the transpension type depend on characteristics of the multiplier. We demonstrate how the transpension type and the strictness axiom can be combined to implement all and improve some of the aforementioned internalization operators (without formal claim in the case of locally fresh names).