The James Construction and π4(S3) in Homotopy Type Theory

被引：0

作者：

Brunerie, Guillaume ^{[1
]}

机构：

[1] Inst Adv Study, Olden Lane, Princeton, NJ 08540 USA

来源：

JOURNAL OF AUTOMATED REASONING | 2019年 / 63卷 / 02期

基金：

美国国家科学基金会;

关键词：

Homotopy type theory; James construction; Agda; Homotopy groups of spheres;

D O I：

10.1007/s10817-018-9468-2

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

In the first part of this paper we present a formalization in Agda of the James construction in homotopy type theory. We include several fragments of code to show what the Agda code looks like, and we explain several techniques that we used in the formalization. In the second part, we use the James construction to give a constructive proof that pi 4(S3) is of the form Z/nZ (but we do not compute the n here).

引用

页码：255 / 284

页数：30