Holonomy classes form a groupoid congruence

Reflexivity, symmetry and transitivity. Two leafwise paths are related exactly when they have the same endpoints and their holonomy germs (computed with the chosen endpoint transversals) are equal. Equality of germs is reflexive, symmetric and transitive by [F3], and having the same endpoints is likewise; hence the relation is an equivalence relation on leafwise paths. Leafwise homotopy relative to endpoints refines it: homotopic relative-endpoint leafwise paths have equal holonomy germs by [F1].

Congruence for concatenation. Suppose $a\sim a^{\mathrm{\prime }}$ and $b\sim b^{\mathrm{\prime }}$, with $a,a^{\mathrm{\prime }}$ from $x$ to $y$ and $b,b^{\mathrm{\prime }}$ from $y$ to $z$, and fix local transversals $T,S,R$ at $x,y,z$. By definition, $h_a(S,T)=h_{a^{\mathrm{\prime }}}(S,T)$ and $h_b(R,S)=h_{b^{\mathrm{\prime }}}(R,S)$. By multiplicativity [F2], $h_{a\ast b}(R,T)=h_b(R,S)\circ h_a(S,T),h_{a^{\mathrm{\prime }}\ast b^{\mathrm{\prime }}}(R,T)=h_{b^{\mathrm{\prime }}}(R,S)\circ h_{a^{\mathrm{\prime }}}(S,T),$ and these composites are equal by the following representative argument, which applies between different transversals. Choose representatives $f,f^{\mathrm{\prime }}:(T,x)\to (S,y)$ agreeing on an open neighborhood $A$ of $x$, and $g,g^{\mathrm{\prime }}:(S,y)\to (R,z)$ agreeing on an open neighborhood $B$ of $y$. By continuity, $A\cap f^{-1}(B)$ is an open neighborhood of $x$; on it $g\circ f=g^{\mathrm{\prime }}\circ f^{\mathrm{\prime }}$, so the composite germs agree by [F3]. Inversion likewise respects germ equality: after restricting the equal representatives $f,f^{\mathrm{\prime }}$ to a neighborhood on which they are diffeomorphisms, their inverses agree on its common open image about $y$. Hence $a\ast b\sim a^{\mathrm{\prime }}\ast b^{\mathrm{\prime }}$: the relation is a congruence.

The quotient is a groupoid. The composite of classes is well defined by step 1.2. Reversal is well defined by [F2] and the representative-inversion argument in step 1.2. The monodromy laws of [F4] supply endpoint-fixed leafwise homotopies from $c_x\ast a$ and $a\ast c_y$ to $a$, from $a\ast a^{-1}$ to $c_x$, and from $a^{-1}\ast a$ to $c_y$, as well as between the two associative concatenations. By step 1.1 these homotopies imply equality of holonomy classes. Thus constant-path classes are identities, reversal gives inverses, and composition is associative, so $\mathrm{Hol}(F)$ is a groupoid.

The projection is a morphism. The projection sends the leafwise homotopy class of a path to its holonomy class; this is well defined by step 1.1 (a homotopy class is contained in a holonomy class), it preserves sources and targets, identities (constant paths), inverses (reversal) and composites (concatenation) by step 1.2 and [F2]. Hence it is a groupoid morphism.