论文标题
同型类型理论中的2个联合等价
2-adjoint equivalences in homotopy type theory
论文作者
论文摘要
我们介绍了（一半）在同型类型理论中（一半）2个联合等价的概念，并证明了它们的预期特性。我们在精益定理供奉献中形式化了这些结果。
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.
