一句话：在同伦类型论中发展胞腔上同调，并在 Agda 中形式化其对有限胞腔复形的计算能力。
本文在同伦类型论中开展胞腔上同调的形式化研究。上同调为空间关联一族阿贝尔群，比同伦群更易计算；胞腔上同调利用胞腔复形逐层粘球面的组合描述来定义这些群。作者的核心结果是：对有限胞腔复形，包括由 Eilenberg-MacLane 空间定义的一类广泛上同调理论，都可通过胞腔上同调计算。该结果已在 Agda 证明助手中完成机器化验证。
We present a development of cellular cohomology in homotopy type theory. Cohomology associates to each space a sequence of abelian groups capturing part of its structure, and has the advantage over homotopy groups in that these abelian groups of many common spaces are easier to compute. Cellular cohomology is a special kind of cohomology designed for cell complexes: these are built in stages by attaching spheres of progressively higher dimension, and cellular cohomology defines the groups out of the combinatorial description of how spheres are attached. Our main result is that for finite cell complexes, a wide class of cohomology theories (including the ones defined through Eilenberg-MacLane spaces) can be calculated via cellular cohomology. This result was formalized in the Agda proof assistant.