[proofplan] Parallel transport is defined by taking endpoints of unique horizontal lifts. We prove each functorial property by constructing an explicit horizontal lift of the relevant path and then invoking uniqueness of horizontal lifts with the same initial point. Constant paths lift to constant paths, reversed lifts remain horizontal because the velocity is multiplied by $-1$, and concatenated lifts are obtained by joining the lift of the first path to the lift of the second. [/proofplan] [step:Identify the horizontal lift of a constant path] Fix $x \in M$ and $p \in P_x$. Define the path \begin{align*} \widetilde{c}_p: [0,1] \to P, \quad t \mapsto p. \end{align*} Then $\pi \circ \widetilde{c}_p = c_x$ and $\widetilde{c}_p(0) = p$. Its velocity is the zero vector: \begin{align*} \dot{\widetilde{c}}_p(t) = 0 \in T_pP. \end{align*} Since each horizontal space $H_p \subset T_pP$ is a vector subspace, $0 \in H_p$, so $\widetilde{c}_p$ is horizontal. By uniqueness of the horizontal lift of $c_x$ starting at $p$, the lift defining parallel transport is $\widetilde{c}_p$. Therefore \begin{align*} \operatorname{PT}_{c_x}(p) = \widetilde{c}_p(1) = p. \end{align*} Since this holds for every $p \in P_x$, we obtain $\operatorname{PT}_{c_x} = \operatorname{id}_{P_x}$. [/step] [step:Reverse a horizontal lift to prove inverse transport] Let $\gamma: [0,1] \to M$ be piecewise smooth, and let $p \in P_{\gamma(0)}$. Define $q := \operatorname{PT}_{\gamma}(p) \in P_{\gamma(1)}$. Let \begin{align*} \widetilde{\gamma}_p: [0,1] \to P \end{align*} be the unique horizontal lift of $\gamma$ with $\widetilde{\gamma}_p(0) = p$, so that $\widetilde{\gamma}_p(1) = q$. Define the reversed lifted path \begin{align*} \widetilde{\bar{\gamma}}_q: [0,1] \to P, \quad t \mapsto \widetilde{\gamma}_p(1-t). \end{align*} Then $\widetilde{\bar{\gamma}}_q(0) = q$, and \begin{align*} \pi(\widetilde{\bar{\gamma}}_q(t)) = \pi(\widetilde{\gamma}_p(1-t)) = \gamma(1-t) = \bar{\gamma}(t). \end{align*} At every parameter value where the derivative exists, the chain rule gives \begin{align*} \dot{\widetilde{\bar{\gamma}}}_q(t) = -\dot{\widetilde{\gamma}}_p(1-t). \end{align*} Because $\widetilde{\gamma}_p$ is horizontal, $\dot{\widetilde{\gamma}}_p(1-t) \in H_{\widetilde{\gamma}_p(1-t)}$. Since $H_{\widetilde{\gamma}_p(1-t)}$ is a vector subspace, its negative also lies in the same horizontal space. Hence $\widetilde{\bar{\gamma}}_q$ is horizontal. By uniqueness, it is the horizontal lift of $\bar{\gamma}$ starting at $q$, and therefore \begin{align*} \operatorname{PT}_{\bar{\gamma}}(q) = \widetilde{\bar{\gamma}}_q(1) = \widetilde{\gamma}_p(0) = p. \end{align*} Thus $\operatorname{PT}_{\bar{\gamma}}(\operatorname{PT}_{\gamma}(p)) = p$ for every $p \in P_{\gamma(0)}$. The same argument applied to $\bar{\gamma}$ gives $\operatorname{PT}_{\gamma}(\operatorname{PT}_{\bar{\gamma}}(r)) = r$ for every $r \in P_{\gamma(1)}$. Hence $\operatorname{PT}_{\bar{\gamma}} = \operatorname{PT}_{\gamma}^{-1}$. [guided] The point is that reversing a curve does not change the line it traces in $P$; it only reverses the direction of its velocity. Fix $p \in P_{\gamma(0)}$ and write $q := \operatorname{PT}_{\gamma}(p)$. By definition of parallel transport, there is a unique horizontal lift \begin{align*} \widetilde{\gamma}_p: [0,1] \to P \end{align*} such that $\pi \circ \widetilde{\gamma}_p = \gamma$, $\widetilde{\gamma}_p(0) = p$, and $\widetilde{\gamma}_p(1) = q$. To construct the lift of the reversed base path, define \begin{align*} \widetilde{\bar{\gamma}}_q: [0,1] \to P, \quad t \mapsto \widetilde{\gamma}_p(1-t). \end{align*} This path starts at $q$ because $\widetilde{\bar{\gamma}}_q(0) = \widetilde{\gamma}_p(1) = q$. It projects to $\bar{\gamma}$ because \begin{align*} \pi(\widetilde{\bar{\gamma}}_q(t)) = \pi(\widetilde{\gamma}_p(1-t)) = \gamma(1-t) = \bar{\gamma}(t). \end{align*} It remains to check horizontality. At every parameter value where the derivative exists, the chain rule gives \begin{align*} \dot{\widetilde{\bar{\gamma}}}_q(t) = -\dot{\widetilde{\gamma}}_p(1-t). \end{align*} The original lift is horizontal, so $\dot{\widetilde{\gamma}}_p(1-t)$ belongs to the horizontal subspace $H_{\widetilde{\gamma}_p(1-t)}$. A horizontal space is a vector subspace of the tangent space at that point, so multiplying a horizontal vector by $-1$ keeps it horizontal. Thus $\widetilde{\bar{\gamma}}_q$ is a horizontal lift of $\bar{\gamma}$ starting at $q$. By uniqueness of horizontal lifts with fixed initial point, this is the lift used to define $\operatorname{PT}_{\bar{\gamma}}$. Therefore \begin{align*} \operatorname{PT}_{\bar{\gamma}}(q) = \widetilde{\bar{\gamma}}_q(1) = \widetilde{\gamma}_p(0) = p. \end{align*} Since $q = \operatorname{PT}_{\gamma}(p)$, this proves $\operatorname{PT}_{\bar{\gamma}} \circ \operatorname{PT}_{\gamma} = \operatorname{id}_{P_{\gamma(0)}}$. Repeating the same argument with $\bar{\gamma}$ in place of $\gamma$ proves $\operatorname{PT}_{\gamma} \circ \operatorname{PT}_{\bar{\gamma}} = \operatorname{id}_{P_{\gamma(1)}}$. Hence $\operatorname{PT}_{\bar{\gamma}}$ is the inverse map of $\operatorname{PT}_{\gamma}$. [/guided] [/step] [step:Concatenate horizontal lifts to prove composition of transports] Let $\gamma_1: [0,1] \to M$ and $\gamma_2: [0,1] \to M$ be piecewise smooth paths with $\gamma_1(1) = \gamma_2(0)$. Fix $p \in P_{\gamma_1(0)}$. Let \begin{align*} \widetilde{\gamma}_{1,p}: [0,1] \to P \end{align*} be the horizontal lift of $\gamma_1$ starting at $p$, and define \begin{align*} q := \widetilde{\gamma}_{1,p}(1) = \operatorname{PT}_{\gamma_1}(p). \end{align*} Let \begin{align*} \widetilde{\gamma}_{2,q}: [0,1] \to P \end{align*} be the horizontal lift of $\gamma_2$ starting at $q$. Define a piecewise smooth path \begin{align*} \widetilde{\Gamma}_p: [0,1] \to P \end{align*} by following $\widetilde{\gamma}_{1,p}$ on the first half of the interval and $\widetilde{\gamma}_{2,q}$ on the second half, with the standard affine reparametrizations. The equality $\widetilde{\gamma}_{1,p}(1) = q = \widetilde{\gamma}_{2,q}(0)$ makes this path continuous at the joining time. Its projection is exactly $\gamma_2 * \gamma_1$, and on each smooth subinterval its velocity is a positive scalar multiple of the velocity of one of the two horizontal lifts. Since horizontal spaces are vector subspaces, positive scalar multiples of horizontal vectors are horizontal. Hence $\widetilde{\Gamma}_p$ is a horizontal lift of $\gamma_2 * \gamma_1$ starting at $p$. By uniqueness of the horizontal lift of $\gamma_2 * \gamma_1$ starting at $p$, the path $\widetilde{\Gamma}_p$ is the lift used to define $\operatorname{PT}_{\gamma_2 * \gamma_1}(p)$. Therefore \begin{align*} \operatorname{PT}_{\gamma_2 * \gamma_1}(p) = \widetilde{\Gamma}_p(1) = \widetilde{\gamma}_{2,q}(1) = \operatorname{PT}_{\gamma_2}(q) = \operatorname{PT}_{\gamma_2}(\operatorname{PT}_{\gamma_1}(p)). \end{align*} Since this holds for every $p \in P_{\gamma_1(0)}$, we conclude \begin{align*} \operatorname{PT}_{\gamma_2 * \gamma_1} = \operatorname{PT}_{\gamma_2} \circ \operatorname{PT}_{\gamma_1}. \end{align*} [/step]