On symmetries of spheres in univalent foundations

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.