Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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.
added this reference
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?)
1 to 5 of 5