Working in univalent foundations, we investigate the symmetries of spheres, i.e., the types of the form $\mathbb{S}^n = \mathbb{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 $\mathbb{Z}/2\mathbb{Z}$ as fundamental group. For the latter result, we develop an EHP long exact sequence.

翻译：在单值基础框架下，我们研究了球面的对称性，即$\mathbb{S}^n = \mathbb{S}^n$形式的类型。圆的情形有一个巧妙结论：圆的对称性构成两个圆的副本。对于更高维的球面，对称类型同样有两个连通分支，即映射度为+1或-1的分支。这两个分支的基本群均为$\mathbb{Z}/2\mathbb{Z}$。为得到后一结论，我们构造了EHP长正合序列。