On symmetries of spheres in univalent foundations

被引：0
|
作者：
Cagne, Pierre [1 ]
Buchholtz, Ulrik [2 ]
Kraus, Nicolai [2 ]
Bezem, Marc [3 ]
机构：
[1] Appalachian State Univ, Boone, NC 28608 USA
[2] Univ Nottingham, Nottingham, England
[3] Univ Bergen, Bergen, Norway
来源：
PROCEEDINGS OF THE 39TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, LICS 2024 | 2024年
关键词：
Type Theory; Univalent Foundations; Symmetries of spheres; EHP sequence;
D O I：
10.1145/3661814.3662115
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form S-n = S-n 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.
引用
收藏
页数：14
相关论文
共 50 条
  • [1] Univalent foundations as structuralist foundations
    Dimitris Tsementzis
    [J]. Synthese, 2017, 194 : 3583 - 3617
  • [2] Univalent foundations as structuralist foundations
    Tsementzis, Dimitris
    [J]. SYNTHESE, 2017, 194 (09) : 3583 - 3617
  • [3] Univalent Foundations of Mathematics
    Voevodsky, Vladimir
    [J]. LOGIC, LANGUAGE, INFORMATION AND COMPUTATION, WOLLIC 2011, 2011, 6642 : 4 - 4
  • [4] Bicategories in univalent foundations
    Ahrens, Benedikt
    Frumin, Dan
    Maggesi, Marco
    Veltri, Niccolo
    van der Weide, Niels
    [J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2022,
  • [5] ON SMALL TYPES IN UNIVALENT FOUNDATIONS
    De Jong, Tom
    Escardo, Martin Hotzel
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2023, 19 (02) : 1 - 33
  • [6] A Descent Property for the Univalent Foundations
    Rijke, Egbert
    [J]. EXTENDED ABSTRACTS FALL 2013: GEOMETRICAL ANALYSIS; TYPE THEORY, HOMOTOPY THEORY AND UNIVALENT FOUNDATIONS, 2015, : 93 - 97
  • [7] Univalent Foundations of Mathematics and Paraconsistency
    Vasyukov, Vladimir L.
    [J]. NEW DIRECTIONS IN PARACONSISTENT LOGIC, 2015, 152 : 285 - 294
  • [8] AN INTRODUCTION TO UNIVALENT FOUNDATIONS FOR MATHEMATICIANS
    Grayson, Daniel R.
    [J]. BULLETIN OF THE AMERICAN MATHEMATICAL SOCIETY, 2018, 55 (04) : 427 - 450
  • [9] GEODESIC SPHERES AND SYMMETRIES
    DATRI, JE
    [J]. NOTICES OF THE AMERICAN MATHEMATICAL SOCIETY, 1975, 22 (05): : A581 - A581
  • [10] Identity and intensionality in Univalent Foundations and philosophy
    Staffan Angere
    [J]. Synthese, 2021, 198 : 1177 - 1217
12345