P2 On symmetries of spheres in univalent foundations
单值基础中的球面对称性
LICS Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science2024匹配度 1/10 · 该论文属于单值基础/同伦类型论中的纯数学结果（球面自同构类型与 EHP 长正合列），虽与类型系统、形式化验证的基础理论相邻，但既不涉及程序静态分析、LLM/Agent，也不涉及浮点或贝叶斯程序分析，与用户的核心研究方向基本无关。引用 5inbox
Pierre Cagne, Ulrik Torben Buchholtz, Nicolai Kraus, Marc Bezem
Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form ####Sn = ####Sn. The case of the circle has a slick answer: the symmetries of the circle form two copies of the circle. For higher-dimensional spheres, the type of symmetries has again two connected components, namely the components of the maps of degree plus or minus one. Each of the two components has Z/2Z as fundamental group. For the latter result, we develop an EHP long exact sequence.
@inproceedings{CagneBKB24,
title = {On symmetries of spheres in univalent foundations},
author = {Pierre Cagne and Ulrik Torben Buchholtz and Nicolai Kraus and Marc Bezem},
booktitle = {LICS},
year = {2024},
doi = {10.1145/3661814.3662115}
}