$pi_2(s^2)$ in HoTT