Language: bi-sorted first order logic with equality and its axiom and additionally the extra-logical primitives: $ ``\tau, < , \in"$, the first is a total unary function on sets denoting is the type of, the rest are binary relations denoting, is lower than and set membership respectively. Sorts are: the first sort in Greek for types, the second sort in ordinary English for sets. Syntatic restrictions include: $\tau$ only taking set symbols as arguments but their values are type symbols, $<$ only occur between type symbols, $\in$ only occur between set symbols.
Axioms:
[A]: Type axioms
Well ordering: $< \text {is a strict well-order on types; that is: } $
$\begin{align} \forall \alpha \forall \beta \, (& \alpha \not < \alpha \\ & \alpha < \beta < \gamma \to \alpha < \gamma \\ & \alpha \neq \beta \to \alpha < \beta \lor \beta < \alpha )\end{align}\\ \exists \alpha (\phi(\alpha)) \to \exists \alpha: \phi(\alpha) \land \neg \exists \beta \, (\phi(\beta) \land \beta < \alpha) $
Infinity: $ \exists \lambda : \exists \alpha (\alpha < \lambda) \land \forall \alpha < \lambda \exists \beta < \lambda \, (\alpha < \beta)$
[B]: Type-Set axioms
Typed Comprehension: if $\phi$ is a formula that does use the symbol $X$, then: $$\forall \alpha \, \exists !X \, \forall y \, (y \in X \iff \tau(y) < \alpha \land \phi)$$
Typing: $ \tau(X)= \min \alpha: \forall y \in X \, ( \alpha > \tau(y))$
Inaccessibility: if $f$ is a definable function, then: $$ \forall X : \neg \, \forall \alpha \, \exists y \, \in X \, (\alpha \leq f(y))$$
Where: $\alpha \leq \beta \iff \alpha < \beta \lor \alpha= \beta$.
Now I think that this theory is a conservative extension over ZF [see here], and over ZFC should Choice be added to it. Moreover, this theory is a naive capture of conceptions about types and sets and portrays a naive enmeshment between them, that it can by itself be considered as motivating $\sf ZF$ set theory. However, what really irks me is that I'm not seeing a simple motivation for Axiom of Choice along type-set lines?
From what I know is that this is not new with me, and the idea of grounding ZF in a kind of type-set theory is old. I want in particular to ask about if there are known simple formulations of axiom of choice in type-set theories, that depends on types in an essential manner?