[proofplan] The [fundamental group](/pages/Fundamental%20Group) $\pi_1(X, x_0)$ is the set of [path homotopy](/pages/Path%20Homotopy) classes of loops at $x_0$, equipped with concatenation of representatives. To prove it is a group we must verify (i) the operation is well defined on classes, (ii) associativity, (iii) existence of an identity, and (iv) existence of inverses. Each property descends from the corresponding law for paths up to path homotopy, because the equivalence relation defining $\pi_1$ is exactly path homotopy rel endpoints. The only content beyond citing the path-level laws is the well-definedness check: concatenation must respect path homotopy. We prove this by composing two homotopies using the pasting lemma. [/proofplan]

[step:Fix the data and recall the operation] Write $I = [0, 1]$. A [loop](/pages/Loop) at $x_0$ is a continuous map $\gamma: I \to X$ with $\gamma(0) = \gamma(1) = x_0$. The set \begin{align*} \pi_1(X, x_0) := \{[\gamma] : \gamma \text{ is a loop at } x_0\} \end{align*} consists of path homotopy classes of such loops, where $[\gamma] = [\gamma']$ means there exists a continuous map $H: I \times I \to X$ with \begin{align*} H(s, 0) = \gamma(s), \quad H(s, 1) = \gamma'(s), \quad H(0, t) = H(1, t) = x_0 \text{ for all } t \in I. \end{align*} The candidate group operation on $\pi_1(X, x_0)$ is defined by \begin{align*} \cdot: \pi_1(X, x_0) \times \pi_1(X, x_0) &\to \pi_1(X, x_0), \\ ([\alpha], [\beta]) &\mapsto [\alpha \cdot \beta], \end{align*} where $\alpha \cdot \beta: I \to X$ is the [path concatenation](/pages/Path%20Concatenation) \begin{align*} (\alpha \cdot \beta)(s) = \begin{cases} \alpha(2s) & 0 \le s \le 1/2, \\ \beta(2s - 1) & 1/2 \le s \le 1. \end{cases} \end{align*} Note that $\alpha \cdot \beta$ is a loop at $x_0$ whenever $\alpha$ and $\beta$ are: continuity follows from the pasting lemma (with agreement $\alpha(1) = x_0 = \beta(0)$ at the splice), and $(\alpha \cdot \beta)(0) = \alpha(0) = x_0$, $(\alpha \cdot \beta)(1) = \beta(1) = x_0$. The identity element is proposed as $e := [c_{x_0}]$, where $c_{x_0}: I \to X$, $s \mapsto x_0$ is the constant loop. The inverse of $[\gamma]$ is proposed as $[\gamma^{-1}]$, where $\gamma^{-1}(s) := \gamma(1 - s)$ is again a loop at $x_0$. [/step]

[step:Prove concatenation is well defined on homotopy classes]Suppose $[\alpha] = [\alpha']$ and $[\beta] = [\beta']$ in $\pi_1(X, x_0)$, witnessed by path homotopies $F, G: I \times I \to X$ with \begin{align*} F(s, 0) &= \alpha(s), & F(s, 1) &= \alpha'(s), & F(0, t) = F(1, t) &= x_0, \\ G(s, 0) &= \beta(s), & G(s, 1) &= \beta'(s), & G(0, t) = G(1, t) &= x_0. \end{align*} Define \begin{align*} H: I \times I &\to X \\ (s, t) &\mapsto \begin{cases} F(2s, t) & 0 \le s \le 1/2, \\ G(2s - 1, t) & 1/2 \le s \le 1. \end{cases} \end{align*} The closed sets $A = \{(s, t) : s \le 1/2\}$ and $B = \{(s, t) : s \ge 1/2\}$ cover $I \times I$. On each, $H$ is the composition of the continuous affine map $(s, t) \mapsto (2s, t)$ (respectively $(s, t) \mapsto (2s - 1, t)$) with the continuous map $F$ (respectively $G$). On the overlap $s = 1/2$, $F(1, t) = x_0 = G(0, t)$, so the two formulas agree. By the [pasting lemma](/pages/Pasting%20Lemma), $H$ is continuous. Verify the boundary conditions: $H(s, 0) = F(2s, 0) = \alpha(2s)$ for $s \le 1/2$ and $G(2s - 1, 0) = \beta(2s - 1)$ for $s \ge 1/2$, hence $H(s, 0) = (\alpha \cdot \beta)(s)$. Similarly $H(s, 1) = (\alpha' \cdot \beta')(s)$. For the fixed-endpoints condition, $H(0, t) = F(0, t) = x_0$ and $H(1, t) = G(1, t) = x_0$ for every $t \in I$. So $H$ is a path homotopy from $\alpha \cdot \beta$ to $\alpha' \cdot \beta'$, giving $[\alpha \cdot \beta] = [\alpha' \cdot \beta']$. Thus $[\alpha] \cdot [\beta]$ is independent of representatives.[/step]

[guided]Why is this a real check? The operation is defined on classes by picking a representative in each class, concatenating, then taking the class of the result. We need the output class to not depend on which representatives we picked. Concretely: if we replace $\alpha$ by $\alpha'$ and $\beta$ by $\beta'$ in the same classes, we must verify $[\alpha \cdot \beta] = [\alpha' \cdot \beta']$. We have, by hypothesis, path homotopies $F$ from $\alpha$ to $\alpha'$ and $G$ from $\beta$ to $\beta'$. The idea is to **concatenate these two homotopies horizontally**: on the left half of $I \times I$ use $F$, on the right half use $G$, each on the appropriately rescaled $s$-variable. \begin{align*} H(s, t) = \begin{cases} F(2s, t) & 0 \le s \le 1/2, \\ G(2s - 1, t) & 1/2 \le s \le 1. \end{cases} \end{align*} **Continuity.** The affine rescaling $s \mapsto 2s$ (resp. $s \mapsto 2s - 1$) is continuous on the closed half $A$ (resp. $B$), and composing with the continuous homotopy $F$ (resp. $G$) yields a continuous function on that half. For the pasting lemma, we need the two pieces to agree on $A \cap B = \{s = 1/2\}$. There, the first branch gives $F(1, t)$ and the second gives $G(0, t)$. Because $F$ is a path homotopy **rel $\{0, 1\}$**, we have $F(1, t) = x_0$ for all $t$; likewise $G(0, t) = x_0$. So both are $x_0$ and they agree. This is the critical place where the "rel endpoints" hypothesis is used. **Values at $t = 0, 1$.** At $t = 0$, the first branch gives $F(2s, 0) = \alpha(2s)$ on $[0, 1/2]$, and the second gives $G(2s - 1, 0) = \beta(2s - 1)$ on $[1/2, 1]$. This is exactly the formula for $\alpha \cdot \beta$. At $t = 1$, we get $\alpha' \cdot \beta'$ by the same calculation. **Rel endpoints.** $H(0, t) = F(0, t) = x_0$, constant in $t$ (because $F$ is rel endpoints at $0$). $H(1, t) = G(1, t) = x_0$, constant in $t$ (similarly). So $H$ is a path homotopy from $\alpha \cdot \beta$ to $\alpha' \cdot \beta'$. **What would fail?** If $F$ and $G$ were general homotopies (not rel endpoints), then at $s = 1/2$ we would have $F(1, t)$ and $G(0, t)$ which would depend on $t$ and in general be unequal, breaking the pasting. The rel-endpoints condition is precisely what makes concatenation of homotopies possible.[/guided]

[step:Deduce associativity from the path-level law] Let $[\alpha], [\beta], [\gamma] \in \pi_1(X, x_0)$ and pick representatives $\alpha, \beta, \gamma$. By the [group laws for paths up to homotopy](/theorems/1877), applied to the paths $\alpha, \beta, \gamma$ (each from $x_0$ to $x_0$, so composable in any order), we have a path homotopy \begin{align*} (\alpha \cdot \beta) \cdot \gamma \simeq \alpha \cdot (\beta \cdot \gamma) \quad \text{rel } \{0, 1\}. \end{align*} Descending to equivalence classes, \begin{align*} ([\alpha] \cdot [\beta]) \cdot [\gamma] = [(\alpha \cdot \beta) \cdot \gamma] = [\alpha \cdot (\beta \cdot \gamma)] = [\alpha] \cdot ([\beta] \cdot [\gamma]). \end{align*} This depends on Step 2, which guarantees that the intermediate expressions $[\alpha] \cdot [\beta] = [\alpha \cdot \beta]$ and $[\beta] \cdot [\gamma] = [\beta \cdot \gamma]$ are unambiguous. [/step]

[step:Deduce the identity law from the path-level law] Let $[\gamma] \in \pi_1(X, x_0)$. By the identity law of [Theorem 1877](/theorems/1877), for any loop $\gamma$ at $x_0$, \begin{align*} \gamma \cdot c_{x_0} \simeq \gamma \simeq c_{x_0} \cdot \gamma \quad \text{rel } \{0, 1\}. \end{align*} Hence $[\gamma] \cdot [c_{x_0}] = [\gamma \cdot c_{x_0}] = [\gamma]$ and $[c_{x_0}] \cdot [\gamma] = [c_{x_0} \cdot \gamma] = [\gamma]$. Therefore $e = [c_{x_0}]$ is a two-sided identity for $\cdot$. [/step]

[step:Deduce the existence of inverses from the path-level law] Let $[\gamma] \in \pi_1(X, x_0)$, so $\gamma$ is a loop at $x_0$. Then $\gamma^{-1}(s) = \gamma(1 - s)$ is also a loop at $x_0$: it is the composition of the continuous map $s \mapsto 1 - s$ with the continuous $\gamma$, and $\gamma^{-1}(0) = \gamma(1) = x_0 = \gamma(0) = \gamma^{-1}(1)$. Applying the inverse law of [Theorem 1877](/theorems/1877) to the loop $\gamma$ (whose endpoints $x_0$ and $x_0$ coincide), \begin{align*} \gamma \cdot \gamma^{-1} \simeq c_{x_0} \quad \text{and} \quad \gamma^{-1} \cdot \gamma \simeq c_{x_0} \quad \text{rel } \{0, 1\}. \end{align*} Passing to classes, $[\gamma] \cdot [\gamma^{-1}] = [c_{x_0}] = e$ and $[\gamma^{-1}] \cdot [\gamma] = [c_{x_0}] = e$. Hence $[\gamma^{-1}]$ is a two-sided inverse of $[\gamma]$. [/step]

[step:Conclude] Step 2 shows the operation $\cdot$ is well defined on $\pi_1(X, x_0)$; Steps 3, 4, and 5 verify associativity, the identity, and the existence of inverses respectively. Therefore $(\pi_1(X, x_0), \cdot, [c_{x_0}])$ satisfies the [group axioms](/pages/Group), completing the proof that the fundamental group is a group. [/step]