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).

翻译：依赖类型理论的预层模型已成功应用于同伦类型论、参数性、定向类型论、守卫类型论及名义类型论的建模。将这些预层模型的某些方面内部化已引起广泛关注，这既可使所得语言更具表达力，亦便于在系统内部进行进一步推理，从而实现更高层次的抽象乃至自动化验证。尽管预层模型的构造大多遵循共通模式，但内部化的实现路径却各不相同。文献中可见多种内部预层算子（$\surd$、$\Phi/\mathsf{extent}$、$\Psi/\mathsf{Gel}$、$\mathsf{Glue}$、$\mathsf{Weld}$、$\mathsf{mill}$、严格性公理及局部新鲜名称），其相对表达能力尚不明确。此外，部分算子要求将类型为形状（可表预层，如区间类型）的变量以仿射方式使用。本文提出一种新型类型构造子——transpension类型，它是对形状进行全称量化的右伴随。其结构类似于同伦类型论中悬垂类型的依赖版本。我们基于称为乘子的基范畴函子，给出了通用的类型规则与预层语义。形状变量的结构规则及transpension类型的某些特性取决于乘子的性质。我们论证了如何结合transpension类型与严格性公理来实现所有前述内部化算子（局部新鲜名称情形无形式化主张），并对部分算子进行了改进。