The Theorem states
6.5.13 A subcategory $D$ of $C$ is a deformation retract of $C$ if and only if $D$ is a full, representative subcategory of $C$. In fact, if $D$ is a full representative subcategory of $C$ and if we define $θx = 1_x$ for each object $x$ of $D$, and choose $θy$ for any other object $y$ of $C$ to be an isomorphism of some $x$ in Ob($D$) with $y$, then $θ$ determines a deformation retraction $r : C → D$ and a homotopy $ir ≃ 1 \ rel \ D$, where $i : D → C$ is the inclusion.
This seems to use some notion of choice for arbitrary categories. Is there some formal justification for this (generalization of AoC) or is the theorem only valid for small categories?
The axiom of choice is indeed talking about sets, which would correspond to small categories. The generalization, which is very often assumed when talking about arbitrary categories, is global choice which simply asserts that the class of all non-empty sets admit a choice function.
Other than just being the "obvious generalization" of the axiom of choice, the justification is that in any "reasonably definable" model of ZFC (e.g. $L[A]$ or $\mathsf{HOD}[X]$) we have a global choice function definable (with parameters, perhaps).
Once we move to categories which are not locally small either, I guess you'd need to apply to second-order choice principles. Those are, again, straightforward generalizations. Here things get a bit trickier, as things often do when moving to second-order logic. So it will depend on how you formalize your second-order set theory.
Of course, one way to avoid all of this is to use universes.