Homotopy Type Theory de Morgan's law > history (Rev #2, changes)

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

is equivalent to

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

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.