Definition Let X be a topological space, and let x₀ and x₁ be points of X.

A path in X from x₀ to x₁ is defined to be a continuous map γ: [0, 1] → X for which γ(0) = x₀ and γ(1) = x₁. A loop in X based at x0 is defined to be a continuous map γ: [0, 1] → X for which γ(0) = γ(1) = x₀.

We can concatenate paths. Let γ₁: [0, 1] → X and γ₂: [0, 1] → X be paths in some topological space X. Suppose that γ₁(1) = γ₂(0). We define theproduct path γ₁.γ₂: [0, 1] → X by

(The continuity of γ1.γ2 may be deduced from Lemma 1.1.)

If γ: [0, 1] → X is a path in X then we define the inverse path γ⁻¹: [0, 1] →X by γ⁻¹ (t) = γ(1−t). (Thus if γ is a path from the point x₀ to the point x1 then γ⁻¹ is the path from x₁ to x₀ obtained by traversing γ in the reverse direction.)

Let X be a topological space, and let x₀ ∈ X be some chosen point of X.

We define an equivalence relation on the set of all (continuous) loops based at the basepoint x₀ of X, where two such loops γ₀ and γ₁ are equivalent if and only if γ₀ ≃ γ₁ rel {0, 1}. We denote the equivalence class of a loop γ: [0, 1] → X based at x₀ by [γ]. This equivalence class is referred to as the based homotopy class of the loop γ. The set of equivalence classes of loops based at x₀ is denoted by π₁(X, x₀). Thus two loops γ₀ and γ₁ represent the same element of π1(X, x₀) if and only if γ₀≃ γ₁ rel {0, 1} (i.e., there exists a homotopy F: [0, 1] × [0, 1] → X between γ₀ and γ₁ which maps (0, τ ) and  (1, τ ) to x₀ for all τ ∈ [0, 1]).

Theorem 1.2 Let X be a topological space, let x0 be some chosen point of X,  and let π₁(X, x₀) be the set of all based homotopy classes of loops based at the point x₀. Then π₁(X, x₀) is a group, the group multiplication on π₁(X, x₀)  being defined according to the rule [γ₁][γ₂] = [γ₁.γ₂] for all loops γ₁ and γ₂ based at x₀.

Proof First we show that the group operation on π1(X, x0) is well-defined.

Let γ₁, γ΄₁, γ₂ and γ΄₂ be loops in X based at the point x₀. Suppose that [γ₁] = [γ΄₁] and [γ₂] = [γ΄₂]. Let the map F: [0, 1] × [0, 1] → X be defined by

where F₁: [0, 1] × [0, 1] → X is a homotopy between γ₁ and γ΄₁, F₂: [0, 1] × [0, 1] → X is a homotopy between γ₂ and γ΄₂, and where the homotopiesF₁ and F₂ map (0, τ ) and (1, τ ) to x₀ for all τ ∈ [0, 1]. Then F is itself a homotopy from γ₁.γ₂ to γ΄₁.γ΄₂, and maps (0, τ ) and (1, τ ) to x₀ for all τ ∈ [0, 1]. Thus [γ₁.γ₂] = [γ΄₁.γ΄₂], showing that the group operation on π₁(X, x₀) is well-defined.

Next we show that the group operation on π₁(X, x₀) is associative. Let γ₁, γ₂ and γ₃ be loops based at x₀, and let α = (γ₁.γ₂).γ₃. Then γ₁.(γ₂.γ₃) = α◦θ,  where

Thus the map G: [0, 1]×[0, 1] → X defined by G(t, τ ) = α((1−τ )t+τθ(t)) is a homotopy between (γ₁.γ₂).γ₃ and γ₁.(γ₂.γ₃), and moreover this homotopy maps (0, τ ) and (1, τ ) to x₀ for all τ ∈ [0, 1]. It follows that (γ₁.γ₂).γ₃ ≃γ₁.(γ₂.γ₃) rel {0, 1} and hence ([γ₁][γ₂])[γ₃] = [γ₁]([γ₂][γ₃]). This shows that the group operation on π₁(X, x₀) is associative.

Let ε: [0, 1] → X denote the constant loop at x0, defined by ε(t) = x₀ for all t ∈ [0, 1]. Then ε.γ = γ ◦ θ₀ and γ.ε = γ ◦ θ₁ for any loop γ based at x₀,  where

r all t ∈ [0, 1]. But the continuous map (t, τ ) → γ((1 − τ )t + τθ_j (t)) is a homotopy between γ and γ ◦ θ_j for j = 0, 1 which sends (0, τ ) and (1, τ )  to x₀ for all τ ∈ [0, 1]. Therefore           ε.γ ≃ γ ≃γ.ε  rel {0, 1}, and hence  [ε][γ] = [γ] = [γ][ε]. We conclude that [ε] represents the identity element of π₁(X, x₀).

It only remains to verify the existence of inverses. Now the map K: [0, 1]×  [0, 1] → X defined by

is a homotopy between the loops γ.γ−1 and ε, and moreover this homotopy

sends (0, τ ) and (1, τ ) to x₀ for all τ ∈ [0, 1]. Therefore γ.γ⁻¹ ≃ ε rel{0, 1}, and thus [γ][γ⁻¹] = [γ.γ⁻¹] = [ε]. On replacing γ by γ⁻¹, we see also that [γ⁻¹][γ] = [ε], and thus [γ⁻¹] = [γ]⁻¹, as required.

Let x₀ be a point of some topological space X. The group π₁(X, x₀) is referred to as the fundamental group of X based at the point x₀.

Let f: X → Y be a continuous map between topological spaces X and Y ,  and let x₀ be a point of X. Then f induces a homomorphism f_#: π₁(X, x0) →π₁(Y, f(x₀)), where                           f_#([γ]) = [f ◦ γ] for all loops γ: [0, 1] → X based at x₀.