一句话：通过 cubical 原语扩展 Agda，使其原生支持 univalence 与高阶归纳类型并保持构造性。
依赖类型证明助手可统一编程与证明，但主流实现缺乏函数外延性、命题外延性等强外延性原则；以公理加入会破坏构造性。Cubical type theory 为 Homotopy Type Theory 与 Univalent Foundations 提供计算解释，使 univalence 与高阶归纳类型具有计算意义。本文把 cubical 原语加入依赖类型函数式语言 Agda，使其成为原生支持 univalence 与一般高阶归纳类型模式的证明助手。由此，函数外延性、命题外延性和商类型可直接定义且有计算内容；结合 copatterns，余归纳类型的 bisimilarity 等价于相等性。该扩展不牺牲类型检查与构造性。
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.
@article{paperbot587,
title = {Cubical agda: a dependently typed programming language with univalence and higher inductive types},
author = {Andrea Vezzosi and Anders Mörtberg and Andreas Abel},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341691}
}