----
> [!definition] Definition. ([[fundamental groupoid]])
> Let $X$ be a [[topological space]]. Consider the set of [[path homotopy]] [[homotopy class|classes]] of the [[equivalence relation]] $\simeq_{p}$. The **fundamental groupoid** is this set, together with the [[partial function]] $*$ that we define now: First, if $f$ is a [[parameterized curve]] in $X$ from $x_{0}$ to $x_{1}$, and $g$ is a [[parameterized curve]] in $X$ from $x_{1}$ to $x_{2}$, then we define their **product path** $f * g$ as the concatenation $(f * g)(s) := \begin{cases}
f(2s) & s \in \left[ 0, \frac{1}{2} \right] \\
g(2s-1) & s \in \left[ \frac{1}{2} ,1 \right].
\end{cases}$
$f *g$ is [[well-defined]] and [[continuous]], by [[the pasting lemma]]; it is a [[parameterized curve]] from $x_{0}$ to $x_{2}$.
\
The product operation on paths induces a [[well-defined]] operation on [[path homotopy|path-homotopy]] [[equivalence class|classes]], defined by the equation $[f] * [g]:= [f * g].$
> [!intuition] The 'positive linear map' interpretation of $*$.
> With the terminology in [[positive linear map]], we can say that $f * g$ is
>- Defined on $\left[ 0, \frac{1}{2} \right]$ as the precomposition of $f$ with the [[positive linear map]] from $\left[ 0, \frac{1}{2} \right]$ to $[0,1]$ (namely, $s \mapsto 2s$);
>- Defined on $\left[ \frac{1}{2}, 1 \right]$ as the precomposition of $g$ with the [[positive linear map]] from $\left[ \frac{1}{2}, 1 \right]$ to $[0,1]$ (namely, $s \mapsto 2s-1$).
> [!justification]
>
> **Well-definition.** First, we need to verify that $[f] * [g]$ is [[well-defined]], i.e., that it does not depend on which representatives we pick. Let $f' \in [f]$ be [[path homotopy|path homotopic]] to $f$ via $F$ and $g' \in [g]$ be [[path homotopy|path homotopic]] to $g$ via $G$. WTS that $f' *g' \simeq_{p} f * g$. Then we define $\begin{align}
> H : & I \times I \to X \\
> H(s,t) := & \begin{cases}
> F(2s,t) & s \in \left[ 0, \frac{1}{2} \right] \\
> G(2s-1,t) & s \in \left[ \frac{1}{2}, 1 \right].
> \end{cases} \end{align}$
> It is easy to see that $H$ is a [[path homotopy]] from $f' * g'$ to $f * g$. For $\begin{align}
> H(s,0) = & \begin{cases}
> F(2s,0) & s \in \left[ 0, \frac{1}{2} \right] \\
> G(2s-1,0) & s \in \left[ \frac{1}{2}, 1 \right]
> \end{cases} = \begin{cases}
> f(2s) & s \in \left[ 0, \frac{1}{2} \right] \\
> g(2s-1) & s \in \left[ \frac{1}{2}, 1 \right]
> \end{cases}= (f * g)(s).
> \end{align}$
> Similarly can verify the other three requirements.
>
> **Right and left identities.** Given $x \in X$, let $e_{x}$ denote the constant [[parameterized curve]] $\begin{align}
> e_{x}: I \to X \\
> t \mapsto x.
> \end{align}$
> We show that if $f$ is a [[parameterized curve]] in $X$ from $x_{0}$ to $x_{1}$, then $[f] * [e_{x_{1}}]=[f] \text{ and } [e_{x_{0}}] * [f]=[f].$
> It is enough to show $f * e_{x_{1}} \cong_{p} f$ and $e_{x_{0}} * f \cong_{p} f$. Let $e_{0}$ denote the constant path *in $I$* at $0$, and we let $i: I \to I$ denote the [[identity map]], which is a [[parameterized curve]] in $I$ from $0$ to $1$. Since $I$ is [[convex]], [[straight-line homotopy|there is]] a [[path homotopy]] $G$ in $I$ between $i$ and $e_{0} * i$. Then $f \circ G$ is a [[path homotopy]] in $X$ between the paths $f \circ i=f$ and $f \circ (e_{0} * i)=(f \circ e_{0}) * (f \circ i)=e_{x_{0}} * f.$
> Similar argument goes through for $e_{x_{1}}$. [[TODO]] bring in picture of graphs
>
> **Inverse.** Given the [[parameterized curve]] $f$ in $X$ from $x_{0}$ to $x_{1}$, let $\overline{f}$ be the [[parameterized curve]] defined by $\overline{f}(s):=f(1-s)$. It is called the **reverse** of $f$. Then $[f] * [\overline{f}] = [e_{x_{0}}] \text{ and } [\overline{f}] * [f]=[e_{x_{1}}].$
> We use a similar approach to the identity proof. The reverse of $i$ is $\overline{i}(s)=1-s$. Since $I$ is [[convex set|convex]], there is a [[path homotopy]] $H$ in $I$ between $e_{0}$ and $i * \overline{i}$. Then $f \circ H$ is a [[path homotopy]] in $X$ between the paths $f \circ e_{0}=e_{x_{0}}$ and $f \circ (i * \overline{i})=(f \circ i) * (f \circ \overline{i})=f * f(1-s) = f * \overline{f}.$
> Similar argument goes through for the other version.
>
> **Associativity.** We want to show that if $[f] * ([g] * [h])$ is [[well-defined]], so is $([f] * [g]) *[h]$, and they are equal. Given paths $f,g,h$ in $X$, the products $f * (g * h)$ and $(f * g) * h$ are defined precisely when $f(1)=g(0)$ and $g(1)=h(0)$. Assuming these two conditions, we define also a "triple product" of the paths $f,g,h$ via the '[[positive linear map]] interpretation of $*