In my search for some type-set 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.

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?

Would adding it to axioms of Type-Set Theory 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$?