On Higher Inductive Types in Cubical Type Theory
On Higher Inductive Types in Cubical Type Theory
复制标题
立方类型理论中的更高归纳类型
DOI：
10.1145/3209108.3209197
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Anders Mörtberg
中科院分区：
文献类型：
--
作者：
T. Coquand;Simon Huber;Anders Mörtberg
立方型理论为同伦型理论的某些方面提供了一个建设性的证明，如Voevodsky的univalence公理。这使得许多外延性原则，如函数和命题外延性，可以在理论中直接证明。本文描述了一个构造性语义，表达在一个预层拓扑结构的适当结构的启发，立方集，一些更高的归纳类型。它还扩展了立方类型理论的语法更高的归纳类型的领域，环面，悬浮液，截断，和推出。所有这些类型都由语义证明，并且对所有构造函数（包括高维构造函数）都有判断计算规则，并且在这些类型形成器下，宇宙是封闭的。
Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. This paper describes a constructive semantics, expressed in a presheaf topos with suitable structure inspired by cubical sets, of some higher inductive types. It also extends cubical type theory by a syntax for the higher inductive types of spheres, torus, suspensions, truncations, and pushouts. All of these types are justified by the semantics and have judgmental computation rules for all constructors, including the higher dimensional ones, and the universes are closed under these type formers.