Fundamental groupoid

Definition

The fundamental groupoid of a topological space $X$ is defined as follows:

As a set, it is the set of all homotopy classes of paths between points in $X$ (i.e., functions from the closed unit interval to $X$ ), where two paths are homotopic if there is a homotopy between them that preserves endpoints at every stage of the homotopy.
The partial multiplication is defined by concatenation of paths where the right endpoint of the left path coincides with the left endpoint of the right path. Specifically, if $f_{1},f_{2}:[0,1]\to X$ are paths, such that $f_{1}(1)=f_{2}(0)$ , then $f_{1}*f_{2}$ is defined as (up to homotopy):

$\!(f_{1}*f_{2})(t)=\lbrace {\begin{array}{rl}f_{1}(2t),&0\leq t\leq 1/2\\f_{2}(2t-1),&1/2<t\leq 1\\\end{array}}$

Condition	How it is shown	Page detailing relevant homotopy
well defined	if $f_{1}$ and $g_{1}$ are homotopic, and $f_{2}$ and $g_{2}$ are homotopic, then the existence of $f_{1}f_{2}$ implies the existence of $g_{1}g_{2}$ , and they are homotopic	homotopy between composites of homotopic paths
existence of identity element	for a path $f$ , the left identity element is a constant loop that stays fixed at $f(0)$ , the right identity is a constant loop that stays fixed at $f(1)$
existence of inverses	for a path $f$ , the inverse path is the path $f^{-1}(t):=f(1-t)$ , that traverses $f$ backward.	similar to the loops case: homotopy between constant loop and composite of loop with inverse
associativity	consider the products $f_{1}(f_{2}f_{3})$ and $(f_{1}f_{2})f_{3}$ . If either of these products is defined, so is the other, and they are homotopic as paths	similar to the loops case: homotopy between composites associated differently