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}$、严格性公理及局部新鲜名称），但关于它们相对表达能力的研究甚少。此外，其中一些算子要求类型为形状（可表预层，例如区间）的变量必须仿射使用。本文提出一种新颖的类型构造子——跨悬置类型，它是在形状上全称量化的右伴随。其结构类似于同伦类型论中悬置类型的依赖版本。我们给出了通用的类型规则，并基于被称为乘子的基范畴函子提供了预层语义。形状变量的结构规则及跨悬置类型的某些特性取决于乘子的特征。我们展示了如何将跨悬置类型与严格性公理结合，以实现所有前述内化算子（对于局部新鲜名称的情况尚无形式化断言）并改进其中部分算子的表达。