同伦类型论中的 James 构造与 $\pi_4(\mathbb{S}^3)$
计算机科学中的逻辑
2017-10-31 v1 代数拓扑
摘要
本文第一部分给出了同伦类型论中 James 构造在 Agda 中的形式化。我们包含了若干代码片段以展示 Agda 代码的形式，并解释了在形式化中使用的几种技术。第二部分中，我们利用 James 构造给出 具有 形式的构造性证明（但此处未计算该 ）。
引用
@article{arxiv.1710.10307,
title = {The James construction and $\pi_4(\mathbb{S}^3)$ in homotopy type theory},
author = {Guillaume Brunerie},
journal= {arXiv preprint arXiv:1710.10307},
year = {2017}
}
备注
30 pages