Refactor shift, pointed identity types are loop spaces

[morphismz]

This pr does two related things:

(i) it shows that pointed identity types are equivalent to loop spaces.

this will be useful in the Eckmann-Hilton and Hopf proof (issue #702), since we can construct an eckmann-hilton term of type $s \cdot s = s \cdot s$, where s is the generator of $\Omega^2 \mathbb{S}^2$`. Then, using this equivalence, we get a term of type $\Omega^3 \mathbb{S}^2$. Due to the way the equivalence is defined, we will get many nice functoriality properties. In particular, the equivalence preserves path concatination. This will be helpful in the proof. It will also later be helpful when applying sypllepsis.

(ii) the pr uses the above equivalenecs to replace unshift in the file universal-property-suspensions-pointed-types