一句话：研究内涵类型论中幂等元的分裂问题，给出可分裂的相干条件并构造不可分裂反例。
本文研究内涵 Martin-Löf 类型论中幂等元何时可分裂。作者证明：在命题截断与 Voevodsky 单值公理下，存在不可分裂的幂等元，因此纯 MLTT 不能证明所有幂等元都分裂；而仅假设函数外延性时，幂等元可分裂当且仅当其幂等性见证满足一个额外相干条件。证明受 Lurie 高阶范畴论启发。作者还证明幂等性见证可从分裂恢复，但该相干条件一般不能，并通过分裂部分相干幂等元类型上的幂等元构造“完全相干幂等元类型”。结果已在 Coq 中形式化验证。
We study idempotents in intensional Martin-L\"of type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodsky's univalence axiom, there exist idempotents that do not split; thus in plain MLTT not all idempotents can be proven to split. On the other hand, assuming only function extensionality, an idempotent can be split if and only if its witness of idempotency satisfies one extra coherence condition. Both proofs are inspired by parallel results of Lurie in higher category theory, showing that ideas from higher category theory and homotopy theory can have applications even in ordinary MLTT. Finally, we show that although the witness of idempotency can be recovered from a splitting, the one extra coherence condition cannot in general; and we construct "the type of fully coherent idempotents", by splitting an idempotent on the type of partially coherent ones. Our results have been formally verified in the proof assistant Coq.