added this reference

- Peter Hilton, p. 289 (9 of 11) in:
*Subjective History of Homology and Homotopy Theory*, Mathematics Magazine**61**5 (1988) 282-291 [doi:10.2307/2689545]

with this quote:

“At a meeting in Vienna in 1931 Čech gave a paper in which he described certain groups from the homotopy point of view. He had no applications of these groups. Moreover, he had only one theorem, that they were commutative. And he was persuaded by people, and we know that Alexandroff played a role here, that they could not be interesting, because it was thought that any information that could be obtained from Abelian groups must come from the homology. Hurewicz redefined the homotopy groups and immediately gave important applications in a series of four notes which were intended as preliminary publications. In that series of four papers he showed the significance of what we now call obstruction theory.”

(Am I linking to the correct “Alexandroff” here?)

]]>I have tried to prettify at *homotopy group* the section *For topological spaces* a little, by introducing Definition/Remark environments etc. Still not fully happy yet, but that’s it for the moment.

I have added to homotopy group a very brief pointer to Mike’s HoTT formalization of $\pi_1(S^1)$.

Eventually I would like to have by default our $n$Lab entries be equipped with detailed pointers to which aspects have been formalized in HoTT (if they have), and in which .v-file precisely.

]]>