一句话：证明高阶归纳类型等式类型的通用路径空间定理，并在 Lean 中形式化。
在 Homotopy Type Theory 中，等式类型的刻画是核心问题，但通常较为困难，已有 encode-decode 等多种方法。本文针对 coequalizer 与 pushout 的等式类型证明了一个类似归纳原则的定理，且不对截断层级施加限制。该结果使得可以直接推理某些等式类型，并消除辅助构造以简化既有证明。作者用它给出了圆周基本群计算的极短论证，证明了 pushout 保持 embedding，并提示了高阶 Seifert–van Kampen 定理：经 set-truncation 后可退化为标准版本。主要技术结果已在证明助手 Lean 中形式化。
The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove a theorem about equality types of coequalizers and pushouts, reminiscent of an induction principle and without any restrictions on the truncation levels. This result makes it possible to reason directly about certain equality types and to streamline existing proofs by eliminating the necessity of auxiliary constructions. To demonstrate this, we give a very short argument for the calculation of the fundamental group of the circle (Licata and Shulman [1]), and for the fact that pushouts preserve embeddings. Further, our development suggests a higher version of the Seifert-van Kampen theorem, and the set-truncation operator maps it to the standard Seifert-van Kampen theorem (due to Favonia and Shulman [2]). We provide a formalization of the main technical results in the proof assistant Lean.