On symmetries of spheres in univalent foundations

Cagne, Pierre; Buchholtz, Ulrik Torben; Kraus, Nicolai; Bezem, Marc

Abstract

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.

Citation

Cagne, P., Buchholtz, U. T., Kraus, N., & Bezem, M. (2024, July). On symmetries of spheres in univalent foundations. Presented at LICS '24: 39th Annual ACM/IEEE Symposium on Logic in Computer Science, Tallinn

• Presentation Conference Type: Edited Proceedings
• Conference Name: LICS '24: 39th Annual ACM/IEEE Symposium on Logic in Computer Science
• Start Date: Jul 8, 2024
• End Date: Jul 11, 2024
• Online Publication Date: Jul 8, 2024
• Publication Date: Jul 8, 2024
• Deposit Date: Oct 3, 2024
• Publicly Available Date: Oct 11, 2024
• Publisher: Association for Computing Machinery (ACM)
• Peer Reviewed: Peer Reviewed
• Pages: 1-14
• Book Title: LICS '24: Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science
• DOI: https://doi.org/10.1145/3661814.3662115
• Keywords: Type Theory, Univalent Foundations, Symmetries of spheres, EHP sequence
• Public URL: https://nottingham-repository.worktribe.com/output/36304679
• Publisher URL: https://dl.acm.org/doi/10.1145/3661814.3662115
• Additional Information: Published: 2024-07-08