%
\label{thm:category-axioms}
$\mathrm{Cat}_\tau$ (Definition~\ref{def:cat-tau}, I.D51)
satisfies the axioms of a category:
\begin{enumerate}
    \item \textbf{Left identity}: for all $\alpha \in \mathrm{Hom}(A, B)$,
          $\mathrm{id}_B \circ \alpha = \alpha$.
    \item \textbf{Right identity}: for all $\alpha \in \mathrm{Hom}(A, B)$,
          $\alpha \circ \mathrm{id}_A = \alpha$.
    \item \textbf{Composition closure}: for all
          $\alpha \in \mathrm{Hom}(A, B)$
          and $\beta \in \mathrm{Hom}(B, C)$,
          the composite $\beta \circ \alpha$
          exists and lies in $\mathrm{Hom}(A, C)$.
    \item \textbf{Associativity}: for all
          $\alpha \in \mathrm{Hom}(A, B)$,
          $\beta \in \mathrm{Hom}(B, C)$,
          $\gamma \in \mathrm{Hom}(C, D)$,
          \[
              (\gamma \circ \beta) \circ \alpha
              = \gamma \circ (\beta \circ \alpha).
          \]
\end{enumerate}

Each axiom follows directly
from the established properties of $\mathrm{HolFun}$.

\textbf{(1) Left identity.}
Let $\alpha = [\pi]_{\mathrm{NF}} \in \mathrm{Hom}(A, B)$.
Then
$\mathrm{id}_B \circ \alpha
= [\mathrm{id}_\tau \circ \pi]_{\mathrm{NF}}
= [\pi]_{\mathrm{NF}}
= \alpha$,
because $\mathrm{id}_\tau \circ \pi = \pi$
as functions on omega-tails.

\textbf{(2) Right identity.}
Similarly,
$\alpha \circ \mathrm{id}_A
= [\pi \circ \mathrm{id}_\tau]_{\mathrm{NF}}
= [\pi]_{\mathrm{NF}}
= \alpha$.

\textbf{(3) Composition closure.}
Let $\alpha = [\pi_\alpha]_{\mathrm{NF}} \in \mathrm{Hom}(A, B)$
and $\beta = [\pi_\beta]_{\mathrm{NF}} \in \mathrm{Hom}(B, C)$.
By Theorem~\ref{thm:composition-closure} (I.T20),
$T_\beta \circ T_\alpha \in \mathrm{HolFun}$.
Therefore $\beta \circ \alpha
= [\pi_\beta \circ \pi_\alpha]_{\mathrm{NF}}
\in \mathrm{Hom}(A, C)$.

\textbf{(4) Associativity.}
By Proposition~\ref{prop:holfun-associativity} (I.P24),
$(T_\gamma \circ T_\beta) \circ T_\alpha
= T_\gamma \circ (T_\beta \circ T_\alpha)$
as functions on omega-tails.
Passing to NF-equivalence classes:
$(\gamma \circ \beta) \circ \alpha
= \gamma \circ (\beta \circ \alpha)$.