论文标题
同型类型理论中的Hurewicz定理
The Hurewicz theorem in Homotopy Type Theory
论文作者
论文摘要
我们证明了Hurewicz定理在同义类型理论中，即，对于$ x $ a的指向，$（n-1）$ - 连接的类型$（n \ geq 1）$和$ a $ a $ a abelian群体，有一个天然的同构$π_n（x）^{ab}^{ab} \ otimes a \ conc $ concy \ tilde a \ tilde a}同源性的同型组的Abelianization。我们还计算了类型的粉碎产品的连通性，并将最低的非平凡同型组作为张量产品。在此过程中，我们研究岩浆，环空间，连接的盖子和前线，并使用$ 1 $合并的类别来表达自然性和Yoneda引理。 由于同型类型理论在所有$ \ infty $ toposes中都具有模型，因此我们的结果可以看作是将空间的已知结果扩展到所有其他$ \ infty $ toposes。
We prove the Hurewicz theorem in homotopy type theory, i.e., that for $X$ a pointed, $(n-1)$-connected type $(n \geq 1)$ and $A$ an abelian group, there is a natural isomorphism $π_n(X)^{ab} \otimes A \cong \tilde{H}_n(X; A)$ relating the abelianization of the homotopy groups with the homology. We also compute the connectivity of a smash product of types and express the lowest non-trivial homotopy group as a tensor product. Along the way, we study magmas, loop spaces, connected covers and prespectra, and we use $1$-coherent categories to express naturality and for the Yoneda lemma. As homotopy type theory has models in all $\infty$-toposes, our results can be viewed as extending known results about spaces to all other $\infty$-toposes.
