同伦类型论中的胞腔上同调
Cellular Cohomology in Homotopy Type Theory
AI总结：
本文在同伦类型论中发展胞腔上同调，证明有限胞腔复形上的一类广泛上同调理论（含艾伦伯格-麦克莱恩空间定义的）可通过胞腔上同调计算，并在Agda中形式化。
摘要：
我们在同伦类型论中提出了胞腔上同调的发展。上同调将每个空间与一个阿贝尔群序列相关联，捕获其部分结构，并且相对于同伦群具有优势，因为许多常见空间的这些阿贝尔群更容易计算。胞腔上同调是一种专为胞腔复形设计的特殊上同调：这些复形通过逐步粘附越来越高维的球面来构建，而胞腔上同调根据球面如何粘附的组合描述来定义这些群。我们的主要结果是，对于有限胞腔复形，一类广泛的上同调理论（包括通过艾伦伯格-麦克莱恩空间定义的那些）可以通过胞腔上同调来计算。这一结果已在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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
