In my search for some [type-set][1] motivated line of thought that might prove axiom of choice, I was thinking of a concept that looks like $\sf V=HOD$, but in terms of types instead of ordinals, that is we think *informally* along the following lines:

$X \text{ is type definable } \iff \\ \exists \alpha_1,.., \exists \alpha_n \exists \phi : \forall y (y \in X \iff \phi(y,\alpha_1,..,\alpha_n))$ 

However, this is known not to be done in first order logic since it involves quantification over all formulas. So, I'll resort to the alterantive approach, which I'll write, paralleling comments by Hamkins, as:

**Type-Definability:** $\forall X \, \exists \theta \, \exists \alpha < \theta \, \exists \varphi :  \forall Y \in V_\theta  ( [V_\theta \models \varphi(X,\alpha)] \iff Y=X).$

Where $V_\theta$ is the set of all sets of type $< \theta$

We'd label that by "type-definable" even though this term had been used in other contexts.

I'd label that as: $\sf V=HTD$, that is all sets are Hereditarily Type Definable.

> Is this formalisable in the language of [Type-Set Theory][1]?

> Would adding it to axioms of [Type-Set Theory][1] prove Axiom of Choice?

> How this would relate to $\sf V=HOD$? Would adding it over the aformentioned Type-Set theory have the same consequences as adding $\sf V=HOD$ over $\sf ZF$?


  [1]: https://math.stackexchange.com/questions/4122497/reference-request-is-axiom-of-choice-motivated-along-type-set-lines?