Skip to main content

Research Repository

Advanced Search

On symmetries of spheres in univalent foundations

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

On symmetries of spheres in univalent foundations Thumbnail


Authors

Pierre Cagne

Dr NICOLAI KRAUS NICOLAI.KRAUS@NOTTINGHAM.AC.UK
Professor of Theoretical Computer Science

Marc Bezem



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

Files





You might also like



Downloadable Citations