Type-theoretic axiom of choice

The type-theoretic axiom of choice (TTAC) is a theorem of dependent type theories with \Sigma and \Pi types. Given types A and B and a family x : A, y : B \vdash R(x, y)\ \textsf{type}, the theorem is a term

  \textsf{ac} :
    \Pi_{x : a} \Sigma_{y : B} R(x, y)
      \to
    \Sigma_{f : A \to B} \Pi_{x : A} R(x, f(x))

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.