On symmetries of spheres in univalent foundations

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}\mathrm{/}2\mathbb{Z}$ as fundamental group. For the latter result, we develop an EHP long exact sequence.