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

翻译：依赖类型论的前层模型已被成功应用于建模HoTT、参数性以及有向、守护和名义类型论。将前层模型的某些方面内化一直备受关注，其目的或是增强语言的表现力，或是在内部进行进一步推理，从而实现更高层次的抽象乃至自动化验证。尽管前层模型的构造大多遵循共同模式，但实现内化的方法却各不相同。文献中出现了多种内部前层算子（$\surd$、$\Phi/\mathsf{extent}$、$\Psi/\mathsf{Gel}$、$\mathsf{Glue}$、$\mathsf{Weld}$、$\mathsf{mill}$、严格性公理和局域新名称），但人们对它们相对表现力的了解甚少。此外，其中一些算子要求类型为形状（可表示的前层，如区间）的变量必须仿射地使用。我们提出一种新型的类型构造器——共维类型（transpension type），它是形状上全称量化的右伴随。其结构类似于HoTT中悬挂类型的依赖版本。我们给出通用类型规则，并基于称为乘子的基范畴函子提供前层语义。形状变量的结构规则以及共维类型的某些方面依赖于乘子的特征。我们展示了如何将共维类型与严格性公理结合，以实现并改进上述所有内化算子（在局域新名称的情形下不作形式化断言）。