标题： AdapTT：依赖类型转换的函子性 显示英文标题

标题： AdapTT: Functoriality for Dependent Type Casts

摘要： 在相关类型之间转换值的能力是许多依赖类型理论变体的共同主题，例如观察类型理论、子类型或渐进类型化的转换演算。 这些转换都表现出一种共同的结构行为，这归结为类型构造器的普遍函子性。 我们提出并深入研究了一种称为AdapTT的类型理论，该理论针对一种抽象的适配器概念，系统且精确地表达了函子类型构造器这一想法。 利用AdapTT中函子归纳类型的描述，我们推导出一般归纳类型构造器上的类型转换的结构定律。 显示英文摘要

摘要： The ability to cast values between related types is a leitmotiv of many flavors of dependent type theory, such as observational type theories, subtyping, or cast calculi for gradual typing. These casts all exhibit a common structural behavior that boils down to the pervasive functoriality of type formers. We propose and extensively study a type theory, called AdapTT, which makes systematic and precise this idea of functorial type formers, with respect to an abstract notion of adapters relating types. Leveraging descriptions for functorial inductive types in AdapTT, we derive structural laws for type casts on general inductive type formers.