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:

**Type-Definability:** $\forall X \ \exists \alpha_1,.., \exists \alpha_n \exists \phi : \forall y (y \in X \iff \phi(y,\alpha_1,..,\alpha_n))$ 

In English: every set is definable by a formula from type parameters. 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?