[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Then one could derive the type theoretic law of excluded middle from the type theoretic law of double negation, as follows. The propositional law of double negation implies propositional excluded middle, which states that for all types $A$, there is an element $\mathrm{lem}_A:[A] \vee \neg [A]$. Since propositional truncation is the same as double negation, and triple negation is the same as a single negation, the type $[A] \vee \neg [A] \equiv [A] \vee \neg \neg \neg A$ is the same as the type $[A] \vee \neg A$. Evaluation of the global choice operator at this element gets the element $\epsilon_{[A] + \neg A}(\mathrm{lem}_A):[A] + \neg A$, and evaluation of the function Suppose that one has $\mathrm{lem}_A:A \vee \neg A$ for all types $A$. Then since it holds for h-propositions, one has classical logic, and in particular, propositional truncations are equivalent to the double negation modality. Thus, $A \vee \neg A$ is the same as $\neg \neg (A + \neg A)$, which is the same as $\neg (\neg A \times \neg \neg A)$. By currying, the latter is the same as $A \to \neg \neg A$. category: redirected to nlab