Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
复制标题
DOI：
10.1145/3341691
复制
发表时间：
2019-08-01
影响因子：
1.8
通讯作者：
Abel, Andreas
中科院分区：
文献类型：
--
作者：
Vezzosi, Andrea;Mortberg, Anders;Abel, Andreas
基于依赖类型理论的证明助理为在同一系统中的编程和证明提供表达语言。但是，所有主要实施都缺乏有关平等推理的强大扩展原则，例如功能和命题扩展。这些原理通常是公理添加的，这破坏了这些系统的建设性。立方体类型理论通过为同型类型理论和单价基础（尤其是单价公理和较高的电感类型）提供计算含义提供了解决方案。本文介绍了具有立方原始素的相关功能编程语言AGDA的扩展，使其成为一名全面的证明助手，并具有对单位的本地支持和较高电感类型的一般模式。这些新的原语使功能和命题扩展性以及可以用计算内容定义的商类型。此外，还要感谢复制图案，双次态度等于相应类型的相等性。这扩展了AGDA，并支持广泛的扩展性原则，而无需牺牲类型检查和建设性。
Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.