Recent work introduced an algorithm and tool in Coq to automatically repair broken proofs in response to changes that correspond to type equivalences. We report on case studies for manual proof repair across type equivalences using an adaptation of this algorithm in Cubical Agda. Crucially, these case studies capture proof repair use cases that were challenging to impossible in prior work in Coq due to type theoretic limitations, highlighting three benefits to working in Cubical Agda: (1) quotient types enrich the space of repairs we can express as type equivalences, (2) dependent path equality makes it possible to internally state and prove correctness of repaired proofs relative to the original proofs, and (3) functional extensionality and transport make it simple to move between slow and fast computations after repair. They also highlight two challenges of working in Cubical Agda, namely those introduced by: (1) lack of tools for automation, and (2) proof relevance, especially as it interacts with definitional equality. We detail these benefits and challenges in hopes to set the stage for later work in proof repair bridging the benefits of both languages.

翻译：近期研究提出了一种在Coq中的算法与工具，用于自动修复因类型等价性变化而损坏的证明。我们报告了在立方体Agda中采用该算法适配方法进行跨类型等价性手动证明修复的案例研究。关键的是，这些案例研究涵盖了在Coq中因类型理论限制而难以甚至无法实现的证明修复用例，突出了在立方体Agda中工作的三个优势：（1）商类型丰富了可表达为类型等价性的修复空间；（2）依赖路径相等性使我们能够内部表述并证明修复后证明相对于原始证明的正确性；（3）函数外延性与传输简化了修复后慢速计算与快速计算之间的切换。同时，这些案例也揭示了立方体Agda中的两个挑战，即：（1）自动化工具缺乏；（2）证明相关性（尤其是与定义相等性交互时）。我们详述了这些优势与挑战，期望为后续弥合两种语言优点的证明修复研究奠定基础。