Pierre Cagne
On symmetries of spheres in univalent foundations
Cagne, Pierre; Buchholtz, Ulrik Torben; Kraus, Nicolai; Bezem, Marc
Authors
Dr ULRIK TORBEN BUCHHOLTZ ULRIK.BUCHHOLTZ@NOTTINGHAM.AC.UK
Assistant Professor
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
On symmetries of spheres in univalent foundations
(749 Kb)
PDF
You might also like
Construction of the circle in UniMath
(2021)
Journal Article
Synthetic fibered (∞,1)-category theory
(2023)
Journal Article
The long exact sequence of homotopy n-groups
(2023)
Journal Article
Epimorphisms and acyclic types in univalent foundations
(2024)
Journal Article
Set-Theoretic and Type-Theoretic Ordinals Coincide
(2023)
Presentation / Conference Contribution
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: discovery-access-systems@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search