Homotopy Type Theory
de Morgan's law

The axiom De Morgan’s Law says that for any $A$ and $B$, if not ($A$ and $B$), then (not $A$) or (not $B$). This is the only one of the four implications making up the classical de Morgan’s laws that is not constructively provable.

Since negations are always propositions?, and propositional truncation? preserves $\times$, in the statement of DML we might as well assume $A$ and $B$ to be propositions. However, it is not quite as obvious whether it matters if the “or” is truncated or not, in other words whether

$$\prod_{A,B} \neg(A \wedge B) \to (\neg A + \neg B)$$

is equivalent to

$$\prod_{A,B} \neg(A \wedge B) \to \Vert \neg A + \neg B\Vert.$$

In fact, these are equivalent by the following argument due to Martin Escardo. Let DML refer to the second, truncated version.

Lemma

DML implies weak? excluded middle?:

$$\prod_{A} \neg A + \neg\neg A.$$

Note that truncation or its absence is irrelevant in WEM, since $\neg A$ and $\neg\neg A$ are mutually exclusive so that $\neg A + \neg\neg A$ is always a proposition.

Proof

Let $B=\neg A$ in DML, and notice that $\neg(A\wedge \neg A)$ always holds.

Lemma

WEM implies that binary sums of negations have split support:

$$\prod_{A,B} \Vert \neg A + \neg B \Vert \to (\neg A + \neg B).$$

Proof

By WEM, either $\neg A$ or $\neg\neg A$. In the first case, $\neg A + \neg B$ is just true. In the second case, either $\neg B$ or $\neg\neg B$. In the first subcase, $\neg A + \neg B$ is again just true. In the second subcase, we have $\neg\neg A$ and $\neg\neg B$, whence $(\neg A + \neg B) = 0$ and in particular is a proposition.

Theorem

DML implies untruncated-DML,

$$\prod_{A,B} \neg(A \wedge B) \to (\neg A + \neg B)$$

Proof

Combine the two lemmas.