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 :  X=\{y \in V_\theta\mid V_\theta\models\varphi(y,\alpha)\}$

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

Note: all term symbols in Greek denote *types* as explained in the linked posting on type-set theory. 

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

I'd label the above axiom 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?