一句话：在同伦类型论中引入（半）2-伴随等价并证明其预期性质，且在 Lean 中形式化。
本文在同伦类型论（HoTT）框架下引入（半）2-伴随等价（(half) 2-adjoint equivalences）这一高阶等价概念，旨在为同伦类型论中的高阶伴随结构提供类型论定义与性质刻画。作者证明该概念所应满足的一系列预期性质，从而推进对同伦类型论中等价理论的理解。所有结果均在 Lean 定理证明器中形式化，给出机器验证的保证。该工作的问题在于如何在同伦类型论中定义并处理（半）2-伴随等价；方法是在 HoTT 中引入定义并证明其性质；评估方式为 Lean 形式化验证。
We introduce the notion of (half) 2-adjoint equivalences in Homotopy Type Theory and prove their expected properties. We formalized these results in the Lean Theorem Prover.
@article{paperbot1348,
title = {2-adjoint equivalences in homotopy type theory},
author = {Daniel Carranza and Jonathan Chang and Chris Kapulkin and Ryan Sandford},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 1},
year = {2021},
doi = {10.23638/lmcs-17(1:3)2021}
}