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)证明相关性（尤其是与定义性相等性交互时）。我们详细阐述了这些优势与挑战，期望为后续融合两种语言优势的证明修复研究奠定基础。