The type-theoretic axiom of choice (TTAC) is a theorem of dependent type theories with and types. Given types and and a family , the theorem is a term
We have a misnomer, in the sense that TTAC is provable in dependent type theory. However, because the axiom of choice is an axiom of similar flavour in set theories, the TTAC retains the name.