Normal coverings and the convention-correct deck quotient

Deck transformations form a group under ordinary composition: associativity is inherited from functions, the identity is over $G$, composites remain over $G$, and $pT=p$ implies $p{T}^{-1}=p$. Evaluation $T\cdot u=T(u)$ is a left action because $1\cdot u=u$ and $(ST)\cdot u=S(T(u))$; it restricts to every fibre since $pT=p$. By pointed classification work in $C_H$. A deck transformation fixing one object fixes every object and arrow: every object is reached by lifting a label from that object, and every arrow is fixed by its source and label. This proves freeness. If it sends $H$ to $Ha$ over $x$, the image of the vertex group there is $a^{-1}Ha$, since $Hag=Ha$ is equivalent to $ag{a}^{-1}\in H$. An invertible functor over $G$ identifies the two vertex groups and their images, so $a^{-1}Ha=H$. Conversely this equality makes $T_a(Hb)=Hab$ and $T_a(Hb,g)=(Hab,g)$ well defined: replacing $b$ by $hb$ replaces $ab$ by $(ah{a}^{-1})ab$. Its inverse is $T_{a^{-1}}$, and the displayed arrow formula verifies it is over $G$.

Transitivity on the fibre over $x$ therefore holds precisely when every $a\in G_x$ normalizes $H$, precisely normality of $H$. Lifting an arrow $g:x\to y$ gives a bijection between the two fibres with inverse the lift of $g^{-1}$; deck transformations commute with these bijections by uniqueness. Thus transitivity on one fibre is equivalent to transitivity on every fibre. When $H$ is normal, every deck transformation is the unique $T_a$ with the specified image of $H$, and $T_a=T_b$ exactly when $Ha=Hb$. Finally $T_a\circ T_b(Hc)=Habc$, also on arrows, so $a\mapsto T_a$ is a surjective homomorphism whose elements sent to the identity are exactly $H$. Since $H$ is normal, $aH=Ha$, and the equality criterion $T_a=T_b$ exactly when $Ha=Hb$ makes $aH\mapsto T_a$ a well-defined bijection. The quotient product $(aH)(bH)=abH$ and the composition calculation show that this bijection preserves products, hence is the claimed group isomorphism. The endpoint prescription is part of this calculation, and would be an antihomomorphism if deck multiplication were instead read left to right.