Transpension：Pi-类型的右伴随
Transpension: The Right Adjoint to the Pi-type
AI总结：
本文提出transpension类型作为形状上全称量化的右伴随，给出类型规则与基于乘子的预层语义，并展示其与严格性公理结合可统一实现并改进多种现有内部化算子。
摘要：
依赖类型论的预层模型已成功应用于建模HoTT、参数性，以及有向、守护和名义类型论。人们对于将这些预层模型的各个方面内部化抱有相当大的兴趣，这要么是为了使所得语言更具表达力，要么是为了在内部进行进一步推理，从而实现更大的抽象，有时还能实现自动化验证。虽然预层模型的构造在很大程度上遵循一个共同的模式，但内部化的方法却并非如此。纵观文献，可以找到各种内部预层算子（$\surd$、$Φ/\mathsf{extent}$、$Ψ/\mathsf{Gel}$、$\mathsf{Glue}$、$\mathsf{Weld}$、$\mathsf{mill}$、严格性公理和局部新鲜名称），而关于它们相对表达力的了解却很少。此外，其中一些算子要求类型为形状（可表示预层，例如区间）的变量以仿射方式使用。我们提出一种新的类型构造子，即transpension类型，它是形状上全称量化的右伴随。其结构类似于HoTT中悬挂类型的依赖版本。我们给出一般类型规则，并依据被称为乘子的基范畴函子给出预层语义。形状变量的结构规则以及transpension类型的某些方面取决于乘子的特征。我们展示了如何将transpension类型与严格性公理相结合，以实现上述所有内部化算子并改进其中一些算子（在局部新鲜名称的情况下不作正式声明）。
英文摘要：
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$, $Φ/\mathsf{extent}$, $Ψ/\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).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
