 \(A^D\) is then defined to be the formula in (vii). Note, however, that these equivalences are not necessarily justified constructively. Only (i) \(\Leftrightarrow\) (ii) and (iii) \(\Leftrightarrow\) (iv) hold constructively whereas (v) \(\Leftrightarrow\) (vi) and (vi) \(\Leftrightarrow\) (vii) are justified constructively only if one also accepts the axiom of choice for all finite types (ACft). Equivalences (ii) \(\Leftrightarrow\) (iii) and (iv) \(\Leftrightarrow\) (v) use a certain amount of classical logic known as the principle of independence of premise (IPft) and Markov’s principle (MPft) for all finite types, respectively. At this point \(A\mapsto A^D\) is just a syntactic translation. But amazingly it gives rise to a meaningful interpretation of HA in T.