HoTT
Explanation of “fundamental group” is confusing
In the introductory text of Chapter 2, in the on-screen PDF version at the bottom of page 59, it reads:
Moreover, the homotopy equivalence classes of loops at some point $x_0$ (where two loops $p$ and $q$ are equated when there is a based homotopy between them, which is a homotopy $H$ as above that additionally satisfies $H(0, t) = H(1, t) = x_0$ for all $t$) form a group called the fundamental group. This group is an algebraic invariant of a space, which can be used to investigate whether two spaces are homotopy equivalent (there are continuous maps back and forth whose composites are homotopic to the identity), because equivalent spaces have isomorphic fundamental groups.
I never had much formal education with topology or algebra. The paragraph is confusing, at least if you come from a background where you don’t already know what a fundamental group is.
The talk is about the loops starting and ending at a specific point $x_0$, which should mean the concept is relative to a point, i.e. the fundamental group is related to a point. Then it says it’s an invariant of the space. That can only be true if the choice of $x_0$ cannot matter, but it doesn’t take much to come up with a space where it does: Take the (disjoint) union of a torus and a sphere. Obviously, all loops of points on the sphere contract under homotopy, but for every point on the torus, there are loops that go around the hole and cannot be contracted.
I’m not sure I can fix this myself because I don’t know what the fundamental group really is, but as-is, it’s confusing and should be rephrased. If I understand it correctly, the fundamental group would be a Σ-type, a concept already explained in Chapter 1, so it’s fair game to refer to it, and at least in the case of a space that’s disconnected, easily a non-trivial Σ-type (where the type of the right-hand side of the pairs really depends on the left-hand side); if the space is path-connected―if I’m not completely mistaken―any point can be moved along a path to any other point, so the choice of base point indeed does not matter. But alas, the paragraph says “space,” not “(path-)connected space.”
