Higher Inductive Types and Internal Parametricity for Cubical Type Theory
Higher Inductive Types and Internal Parametricity for Cubical Type Theory
复制标题
立方型理论的更高归纳型和内部参数性
DOI：
10.1184/r1/14555691.v1
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Evan Cavallo
中科院分区：
文献类型：
--
作者：
Evan Cavallo
类型理论设计的最新创新（以建设性为重点的数学制度）产生了间隔变量的概念，可用于捕获携带计算内容的对象之间的关系。在参数解释中应用的平等，特别是Quotients和任意关系。包含的内容平等，包括立方体类型的理论。在类型理论中，长期存在的不足。同型理论称为较高的归纳类型，将归纳类型和引用的概念融合在一起。基于构造保留对象之间的所有关系的想法，以类型理论执行的构建属性工具，最近的工作表明，可以使用基于间隔的系统将参数属性集成到类型理论中。立方平等的行为改善了内部参数的行为，并将内部参数作为解决方案理论的困难问题。凝聚力模化是为了表达参数类型和非参数类型理论之间的相互作用，从而在非参数设置中可以使用参数结果。
Recent innovation in the design of type theories—foundational systems of mathematics with a focus on constructivity—has produced the concept of interval variable, which can be used to capture relations between objects that carry computational content. We examine two such relationships in type theory: equality, in particularquotients, and arbitrary relations as applied in parametricity interpretations. Cubical type theory, a system using an interval-based formulation of equality, enables a permissive kind of content-carrying equality that includes in particularisomorphism. Cubical type theory provides a constructive interpretation of homotopy type theory and the Univalent Foundations, formalisms that introduced the idea of isomorphism as equality but which lack intrinsic computational meaning. The cubical approach to equality also rectifies long-standing deficiencies in the behavior ofquotients in type theory. We realize a system of generalized quotients for cubical type theory originally conceived in homotopy type theory, called higher inductive types, that merges the concepts of inductive type and quotient. Such a mutual generalization is particularly essential in the contentful equality setting, but also has significant applications to ordinary mathematics. Parametricity is, among other things, a proof technique for deriving propertiesof constructions performed in type theories, based on the idea that constructions preserve all relations between objects. Traditionally a meta-theoretical tool, recentwork has shown that parametricity properties can be integrated into a type theory itself using an interval-based system. We develop internal parametricity on top ofcubical type theory, examining the similarities and distinctions between the two applications of intervals, finding that a background of cubical equality improves thebehavior of internal parametricity, and applying internal parametricity as a tool to solve difficult problems in cubical type theory. We introduce a system of cohesionmodalities to express the interaction between parametric and non-parametric type theory, enabling the use of parametricity results in a non-parametric setting.