Martin Escardo.

Excluded middle related things. Notice that this file doesn't
postulate excluded middle. It only defines what the principle of
excluded middle is.

In the Curry-Howard interpretation, excluded middle say that every
type has an inhabitant or os empty. In univalent foundations, where
one works with propositions as subsingletons, excluded middle is the
principle that every subsingleton type is inhabited or empty.

\begin{code}

{-# OPTIONS --safe --without-K #-}

module UF.ClassicalLogic where

open import MLTT.Spartan

open import UF.Base
open import UF.Equiv
open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier
open import UF.UniverseEmbedding

\end{code}

Excluded middle (EM) is not provable or disprovable. However, we do
have that there is no truth value other than false (⊥) or true (⊤),
which we refer to as the density of the decidable truth values.

\begin{code}

EM : ∀ 𝓤 → 𝓤 ⁺ ̇
EM 𝓤 = (P : 𝓤 ̇ ) → is-prop P → P + ¬ P

excluded-middle = EM

lower-EM : ∀ 𝓥 → EM (𝓤 ⊔ 𝓥) → EM 𝓤
lower-EM 𝓥 em P P-is-prop = f d
 where
  d : Lift 𝓥 P + ¬ Lift 𝓥 P
  d = em (Lift 𝓥 P) (equiv-to-prop (Lift-is-universe-embedding 𝓥 P) P-is-prop)

  f : Lift 𝓥 P + ¬ Lift 𝓥 P → P + ¬ P
  f (inl p) = inl (lower p)
  f (inr ν) = inr (λ p → ν (lift 𝓥 p))

Excluded-Middle : 𝓤ω
Excluded-Middle = ∀ {𝓤} → EM 𝓤

EM-is-prop : FunExt → is-prop (EM 𝓤)
EM-is-prop {𝓤} fe = Π₂-is-prop
                     (λ {𝓤} {𝓥} → fe 𝓤 𝓥)
                     (λ _ → decidability-of-prop-is-prop (fe 𝓤 𝓤₀))

LEM : ∀ 𝓤 → 𝓤 ⁺ ̇
LEM 𝓤 = (p : Ω 𝓤) → p holds + ¬ (p holds)

EM-gives-LEM : EM 𝓤 → LEM 𝓤
EM-gives-LEM em p = em (p holds) (holds-is-prop p)

LEM-gives-EM : LEM 𝓤 → EM 𝓤
LEM-gives-EM lem P i = lem (P , i)

\end{code}

Added by Martin Escardo and Tom de Jong 29th August 2024. Originally
we worked with WEM. But it turns out that it is not necessary to
assume that P is a proposition, and so we now work with the new
definition typal-WEM, which removes this assumption.

\begin{code}

WEM : ∀ 𝓤 → 𝓤 ⁺ ̇
WEM 𝓤 = (P : 𝓤 ̇ ) → is-prop P → ¬ P + ¬¬ P

typal-WEM : ∀ 𝓤 → 𝓤 ⁺ ̇
typal-WEM 𝓤 = (A : 𝓤 ̇ ) → ¬ A + ¬¬ A

WEM-gives-typal-WEM : funext 𝓤 𝓤₀ → WEM 𝓤 → typal-WEM 𝓤
WEM-gives-typal-WEM fe wem' A =
 Cases (wem' (¬ A) (negations-are-props fe))
  inr
  (inl ∘ three-negations-imply-one)

typal-WEM-gives-WEM : typal-WEM 𝓤 → WEM 𝓤
typal-WEM-gives-WEM wem P P-is-prop = wem P

typal-WEM-is-prop : FunExt → is-prop (typal-WEM 𝓤)
typal-WEM-is-prop {𝓤} fe = Π-is-prop (fe (𝓤 ⁺) 𝓤)
                            (λ _ → decidability-of-prop-is-prop (fe 𝓤 𝓤₀)
                                    (negations-are-props (fe 𝓤 𝓤₀)))

WEM-is-prop : FunExt → is-prop (WEM 𝓤)
WEM-is-prop {𝓤} fe = Π₂-is-prop (λ {𝓥} {𝓦} → fe 𝓥 𝓦)
                       (λ _ _ → decidability-of-prop-is-prop (fe 𝓤 𝓤₀)
                                 (negations-are-props (fe 𝓤 𝓤₀)))

\end{code}

End of addition.

Double negation elimination is equivalent to excluded middle.

\begin{code}

DNE : ∀ 𝓤 → 𝓤 ⁺ ̇
DNE 𝓤 = (P : 𝓤 ̇ ) → is-prop P → ¬¬ P → P

EM-gives-DNE : EM 𝓤 → DNE 𝓤
EM-gives-DNE em P i φ = cases id (λ u → 𝟘-elim (φ u)) (em P i)

double-negation-elim : EM 𝓤 → DNE 𝓤
double-negation-elim = EM-gives-DNE

fake-¬¬-EM : {X : 𝓤 ̇ } → ¬¬ (X + ¬ X)
fake-¬¬-EM u = u (inr (λ p → u (inl p)))

DNE-gives-EM : funext 𝓤 𝓤₀ → DNE 𝓤 → EM 𝓤
DNE-gives-EM fe dne P isp = dne (P + ¬ P)
                             (decidability-of-prop-is-prop fe isp)
                             fake-¬¬-EM

all-props-negative-gives-DNE : funext 𝓤 𝓤₀
                            → ((P : 𝓤 ̇ ) → is-prop P → Σ Q ꞉ 𝓤 ̇ , (P ↔ ¬ Q))
                            → DNE 𝓤
all-props-negative-gives-DNE {𝓤} fe ϕ P P-is-prop = I (ϕ P P-is-prop)
 where
  I : (Σ Q ꞉ 𝓤 ̇ , (P ↔ ¬ Q)) → ¬¬ P → P
  I (Q , f , g) ν = g (three-negations-imply-one (double-contrapositive f ν))

all-props-negative-gives-EM
 : funext 𝓤 𝓤₀
 → ((P : 𝓤 ̇ ) → is-prop P → Σ Q ꞉ 𝓤 ̇ , (P ↔ ¬ Q))
 → EM 𝓤
all-props-negative-gives-EM {𝓤} fe ϕ
 = DNE-gives-EM fe (all-props-negative-gives-DNE fe ϕ)

fe-and-em-give-propositional-truncations
 : FunExt
 → Excluded-Middle
 → propositional-truncations-exist
fe-and-em-give-propositional-truncations fe em =
 record {
  ∥_∥          = λ X → ¬¬ X ;
  ∥∥-is-prop   = Π-is-prop (fe _ _) (λ _ → 𝟘-is-prop) ;
  ∣_∣          = λ x u → u x ;
  ∥∥-rec       = λ i u φ → EM-gives-DNE em _ i (¬¬-functor u φ)
 }

\end{code}

We now consider various logically equivalent formulations of De Morgan
Law.

\begin{code}

untruncated-De-Morgan : ∀ 𝓤 → 𝓤 ⁺ ̇
untruncated-De-Morgan 𝓤 = (P Q : 𝓤 ̇ )
                        → is-prop P
                        → is-prop Q
                        → ¬ (P × Q) → ¬ P + ¬ Q

EM-gives-untruncated-De-Morgan : EM 𝓤
                               → untruncated-De-Morgan 𝓤
EM-gives-untruncated-De-Morgan em A B i j =
 λ (ν : ¬ (A × B)) →
      Cases (em A i)
       (λ (a : A) → Cases (em B j)
                     (λ (b : B) → 𝟘-elim (ν (a , b)))
                     inr)
       inl

\end{code}

But already weak excluded middle gives De Morgan.

Added/modified by Martin Escardo and Tom de Jong 29th August 2024. A typal
version of De Morgan.

\begin{code}

non-contradiction : {X : 𝓤 ̇ } → ¬ (X × ¬ X)
non-contradiction (x , ν) = ν x

untruncated-typal-De-Morgan : ∀ 𝓤 → 𝓤 ⁺ ̇
untruncated-typal-De-Morgan 𝓤 = (P Q : 𝓤 ̇ ) → ¬ (P × Q) → ¬ P + ¬ Q

untruncated-typal-De-Morgan-gives-untruncated-De-Morgan
 : untruncated-typal-De-Morgan 𝓤
 → untruncated-De-Morgan 𝓤
untruncated-typal-De-Morgan-gives-untruncated-De-Morgan d' P Q i j = d' P Q

\end{code}

Originally the following was proved with WEM.

\begin{code}

typal-WEM-gives-untruncated-typal-De-Morgan : typal-WEM 𝓤
                                            → untruncated-typal-De-Morgan 𝓤
typal-WEM-gives-untruncated-typal-De-Morgan wem A B =
 λ (ν : ¬ (A × B)) →
      Cases (wem A)
       inl
       (λ (ϕ : ¬¬ A)
             → Cases (wem B)
                inr
                (λ (γ : ¬¬ B) → 𝟘-elim
                                 (ϕ (λ (a : A) → γ (λ (b : B) → ν (a , b))))))

typal-WEM-gives-untruncated-De-Morgan : typal-WEM 𝓤 → untruncated-De-Morgan 𝓤
typal-WEM-gives-untruncated-De-Morgan =
 untruncated-typal-De-Morgan-gives-untruncated-De-Morgan
 ∘ typal-WEM-gives-untruncated-typal-De-Morgan

untruncated-De-Morgan-gives-WEM : funext 𝓤 𝓤₀
                                → untruncated-De-Morgan 𝓤
                                → WEM 𝓤
untruncated-De-Morgan-gives-WEM fe d P i =
 d P (¬ P) i (negations-are-props fe) non-contradiction

untruncated-De-Morgan-gives-typal-WEM : funext 𝓤 𝓤₀
                                      → untruncated-De-Morgan 𝓤
                                      → typal-WEM 𝓤
untruncated-De-Morgan-gives-typal-WEM fe =
 WEM-gives-typal-WEM fe ∘ untruncated-De-Morgan-gives-WEM fe

untruncated-De-Morgan-gives-untruncated-typal-De-Morgan
 : funext 𝓤 𝓤₀
 → untruncated-De-Morgan 𝓤
 → untruncated-typal-De-Morgan 𝓤
untruncated-De-Morgan-gives-untruncated-typal-De-Morgan fe =
 typal-WEM-gives-untruncated-typal-De-Morgan
 ∘ untruncated-De-Morgan-gives-typal-WEM fe

\end{code}

End of addition/modification.

Is the above untruncated De Morgan Law a proposition? Not in
general. If it doesn't hold, it is vacuously a proposition. But if it
does hold, it is not a proposition. We prove this by modifying any
given δ : De-Mordan 𝓤 to a different δ' : untruncated-De-Morgan
𝓤. Then we also consider a truncated version of untruncated-De-Morgan
that is a proposition and is logically equivalent to
untruncated-De-Morgan. So untruncated-De-Morgan 𝓤 is not necessarily a
proposition, but it always has split support (it has a proposition as
a retract).

\begin{code}

untruncated-De-Morgan-is-prop
 : ¬ untruncated-De-Morgan 𝓤
 → is-prop (untruncated-De-Morgan 𝓤)
untruncated-De-Morgan-is-prop ν δ = 𝟘-elim (ν δ)

untruncated-typal-De-Morgan-has-two-witnesses-if-it-has-one
 : funext 𝓤 𝓤₀
 → (δ : untruncated-typal-De-Morgan 𝓤)
 → Σ δ' ꞉ untruncated-typal-De-Morgan 𝓤 , δ' ≠ δ
untruncated-typal-De-Morgan-has-two-witnesses-if-it-has-one {𝓤} fe δ
 = (δ' , III)
 where
  open import MLTT.Plus-Properties

  wem : typal-WEM 𝓤
  wem = untruncated-De-Morgan-gives-typal-WEM fe
         (untruncated-typal-De-Morgan-gives-untruncated-De-Morgan δ)

  g : (P Q : 𝓤 ̇ )
      (ν : ¬ (P × Q))
      (a : ¬ P + ¬¬ P)
      (b : ¬ Q + ¬¬ Q)
      (c : ¬ P + ¬ Q)
    → ¬ P + ¬ Q
  g P Q ν (inl _) (inl v) (inl _) = inr v
  g P Q ν (inl u) (inl _) (inr _) = inl u
  g P Q ν (inl _) (inr _) _       = δ P Q ν
  g P Q ν (inr _) _       _       = δ P Q ν

  δ' : untruncated-typal-De-Morgan 𝓤
  δ' P Q ν = g P Q ν (wem P) (wem Q) (δ P Q ν)

  I : (h : ¬ 𝟘) → wem 𝟘 ＝ inl h
  I h = I₀ (wem 𝟘) refl
   where
    I₀ : (a : ¬ 𝟘 + ¬¬ 𝟘) → wem 𝟘 ＝ a → wem 𝟘 ＝ inl h
    I₀ (inl u) = transport
                  (λ - → wem 𝟘 ＝ inl -)
                  (negations-are-props fe u h)
    I₀ (inr ϕ) p = 𝟘-elim (ϕ h)

  ν : ¬ (𝟘 × 𝟘)
  ν (p , q) = 𝟘-elim p

  II : δ' 𝟘 𝟘 ν ≠ δ 𝟘 𝟘 ν
  II = II₃
   where
    m n : ¬ 𝟘 + ¬ 𝟘
    m = δ 𝟘 𝟘 ν
    n = g 𝟘 𝟘 ν (inl 𝟘-elim) (inl 𝟘-elim) m

    II₁ : δ' 𝟘 𝟘 ν ＝ n
    II₁ = ap₂ (λ -₁ -₂ → g 𝟘 𝟘 ν -₁ -₂ m)
              (I 𝟘-elim)
              (I 𝟘-elim)

    II₂ : (m' : ¬ 𝟘 + ¬ 𝟘)
        → m ＝ m'
        → g 𝟘 𝟘 ν (inl 𝟘-elim) (inl 𝟘-elim) m' ≠ m
    II₂ (inl x) p q = +disjoint
                       (inl x      ＝⟨ p ⁻¹ ⟩
                        m          ＝⟨ q ⁻¹ ⟩
                        inr 𝟘-elim ∎)
    II₂ (inr x) p q = +disjoint
                       (inl 𝟘-elim ＝⟨ q ⟩
                        m          ＝⟨ p ⟩
                        inr x      ∎)

    II₃ : δ' 𝟘 𝟘 ν ≠ m
    II₃ = transport (_≠ m) (II₁ ⁻¹) (II₂ m refl)

  III : δ' ≠ δ
  III e = II III₀
   where
    III₀ : δ' 𝟘 𝟘 ν ＝ δ 𝟘 𝟘 ν
    III₀ = ap (λ - → - 𝟘 𝟘 ν) e

untruncated-typal-De-Morgan-is-not-prop
 : funext 𝓤 𝓤₀
 → untruncated-typal-De-Morgan 𝓤
 → ¬ is-prop (untruncated-typal-De-Morgan 𝓤)
untruncated-typal-De-Morgan-is-not-prop {𝓤} fe δ
 = IV (untruncated-typal-De-Morgan-has-two-witnesses-if-it-has-one fe δ)
 where
  IV : (Σ δ' ꞉ untruncated-typal-De-Morgan 𝓤 , δ' ≠ δ)
    → ¬ is-prop (untruncated-typal-De-Morgan 𝓤)
  IV (δ' , III) i = III (i δ' δ)

\end{code}

We repeat the above proof adding more information.

TODO. Is it possible to prove the following from the above, or
vice-versa, to avoid the repetition?

\begin{code}

untruncated-De-Morgan-has-at-least-two-witnesses-if-it-has-one
 : funext 𝓤 𝓤₀
 → (δ : untruncated-De-Morgan 𝓤)
 → Σ δ' ꞉ untruncated-De-Morgan 𝓤 , δ' ≠ δ
untruncated-De-Morgan-has-at-least-two-witnesses-if-it-has-one {𝓤} fe δ
 = (δ' , III)
 where
  open import MLTT.Plus-Properties

  wem : typal-WEM 𝓤
  wem = untruncated-De-Morgan-gives-typal-WEM fe δ

  g : (P Q : 𝓤 ̇ )
      (i : is-prop P) (j : is-prop Q)
      (ν : ¬ (P × Q))
      (a : ¬ P + ¬¬ P)
      (b : ¬ Q + ¬¬ Q)
      (c : ¬ P + ¬ Q)
    → ¬ P + ¬ Q
  g P Q i j ν (inl _) (inl v) (inl _) = inr v
  g P Q i j ν (inl u) (inl _) (inr _) = inl u
  g P Q i j ν (inl _) (inr _) _       = δ P Q i j ν
  g P Q i j ν (inr _) _       _       = δ P Q i j ν

  δ' : untruncated-De-Morgan 𝓤
  δ' P Q i j ν = g P Q i j ν (wem P) (wem Q) (δ P Q i j ν)

  I : (i : is-prop 𝟘) (h : ¬ 𝟘) → wem 𝟘 ＝ inl h
  I i h = I₀ (wem 𝟘) refl
   where
    I₀ : (a : ¬ 𝟘 + ¬¬ 𝟘) → wem 𝟘 ＝ a → wem 𝟘 ＝ inl h
    I₀ (inl u) = transport
                  (λ - → wem 𝟘 ＝ inl -)
                  (negations-are-props fe u h)
    I₀ (inr ϕ) p = 𝟘-elim (ϕ h)

  ν : ¬ (𝟘 × 𝟘)
  ν (p , q) = 𝟘-elim p

  II : (i j : is-prop 𝟘) → δ' 𝟘 𝟘 i j ν ≠ δ 𝟘 𝟘 i j ν
  II i j = II₃
   where
    m n : ¬ 𝟘 + ¬ 𝟘
    m = δ 𝟘 𝟘 i j ν
    n = g 𝟘 𝟘 i j ν (inl 𝟘-elim) (inl 𝟘-elim) m

    II₁ : δ' 𝟘 𝟘 i j ν ＝ n
    II₁ = ap₂ (λ -₁ -₂ → g 𝟘 𝟘 i j ν -₁ -₂ m)
              (I i 𝟘-elim)
              (I j 𝟘-elim)

    II₂ : (m' : ¬ 𝟘 + ¬ 𝟘)
        → m ＝ m'
        → g 𝟘 𝟘 i j ν (inl 𝟘-elim) (inl 𝟘-elim) m' ≠ m
    II₂ (inl x) p q = +disjoint
                       (inl x      ＝⟨ p ⁻¹ ⟩
                        m          ＝⟨ q ⁻¹ ⟩
                        inr 𝟘-elim ∎)
    II₂ (inr x) p q = +disjoint
                       (inl 𝟘-elim ＝⟨ q ⟩
                        m          ＝⟨ p ⟩
                        inr x      ∎)

    II₃ : δ' 𝟘 𝟘 i j ν ≠ m
    II₃ = transport (_≠ m) (II₁ ⁻¹) (II₂ m refl)

  III : δ' ≠ δ
  III e = II 𝟘-is-prop 𝟘-is-prop III₀
   where
    III₀ : δ' 𝟘 𝟘 𝟘-is-prop 𝟘-is-prop ν ＝ δ 𝟘 𝟘 𝟘-is-prop 𝟘-is-prop ν
    III₀ = ap (λ - → - 𝟘 𝟘 𝟘-is-prop 𝟘-is-prop ν) e

untruncated-De-Morgan-is-not-prop
 : funext 𝓤 𝓤₀
 → untruncated-De-Morgan 𝓤
 → ¬ is-prop (untruncated-De-Morgan 𝓤)
untruncated-De-Morgan-is-not-prop {𝓤} fe δ
 = IV (untruncated-De-Morgan-has-at-least-two-witnesses-if-it-has-one fe δ)
 where
  IV : (Σ δ' ꞉ untruncated-De-Morgan 𝓤 , δ' ≠ δ)
    → ¬ is-prop (untruncated-De-Morgan 𝓤)
  IV (δ' , III) i = III (i δ' δ)

untruncated-De-Morgan-curiousity : funext 𝓤 𝓤₀
                                 → ¬¬ is-prop (untruncated-De-Morgan 𝓤)
                                 → is-prop (untruncated-De-Morgan 𝓤)
untruncated-De-Morgan-curiousity fe =
 untruncated-De-Morgan-is-prop
 ∘ contrapositive (untruncated-De-Morgan-is-not-prop fe)

module _ (pt : propositional-truncations-exist) where

 open PropositionalTruncation pt

 typal-De-Morgan : ∀ 𝓤 → 𝓤 ⁺ ̇
 typal-De-Morgan 𝓤 = (P Q : 𝓤 ̇ ) → ¬ (P × Q) → ¬ P ∨ ¬ Q

 De-Morgan : ∀ 𝓤 → 𝓤 ⁺ ̇
 De-Morgan 𝓤 = (P Q : 𝓤 ̇ )
             → is-prop P
             → is-prop Q
             → ¬ (P × Q) → ¬ P ∨ ¬ Q

 typal-De-Morgan-is-prop : FunExt
                         → is-prop (typal-De-Morgan 𝓤)
 typal-De-Morgan-is-prop fe = Π₃-is-prop (λ {𝓤} {𝓥} → fe 𝓤 𝓥)
                                         (λ P Q ν → ∨-is-prop)

 De-Morgan-is-prop : FunExt → is-prop (De-Morgan 𝓤)
 De-Morgan-is-prop fe = Π₅-is-prop (λ {𝓤} {𝓥} → fe 𝓤 𝓥)
                                   (λ P Q i j ν → ∨-is-prop)

 untruncated-De-Morgan-gives-De-Morgan : untruncated-De-Morgan 𝓤
                                       → De-Morgan 𝓤
 untruncated-De-Morgan-gives-De-Morgan d P Q i j ν = ∣ d P Q i j ν ∣

 De-Morgan-gives-WEM : funext 𝓤 𝓤₀
                     → De-Morgan 𝓤
                     → WEM 𝓤
 De-Morgan-gives-WEM {𝓤} fe dm P i = III
  where
   I : ¬ (P × ¬ P) → ¬ P ∨ ¬¬ P
   I = dm P (¬ P) i (negations-are-props fe)

   II : ¬ P ∨ ¬¬ P
   II = I non-contradiction

   III : ¬ P + ¬¬ P
   III = exit-∥∥
          (decidability-of-prop-is-prop fe (negations-are-props fe))
          II

 De-Morgan-gives-typal-WEM : funext 𝓤 𝓤₀ → De-Morgan 𝓤 → typal-WEM 𝓤
 De-Morgan-gives-typal-WEM {𝓤} fe =
  WEM-gives-typal-WEM fe ∘ De-Morgan-gives-WEM fe

 De-Morgan-gives-untruncated-De-Morgan : funext 𝓤 𝓤₀
                                       → De-Morgan 𝓤
                                       → untruncated-De-Morgan 𝓤
 De-Morgan-gives-untruncated-De-Morgan fe t P Q i j ν =
  typal-WEM-gives-untruncated-De-Morgan
   (De-Morgan-gives-typal-WEM fe t)
   P Q i j ν

 typal-De-Morgan-gives-De-Morgan : typal-De-Morgan 𝓤 → De-Morgan 𝓤
 typal-De-Morgan-gives-De-Morgan d P Q i j = d P Q

 untruncated-typal-De-Morgan-gives-typal-De-Morgan
  : untruncated-typal-De-Morgan 𝓤
  → typal-De-Morgan 𝓤
 untruncated-typal-De-Morgan-gives-typal-De-Morgan d P Q ν =
  ∣ d P Q ν ∣

 De-Morgan-gives-typal-De-Morgan : funext 𝓤 𝓤₀
                                 → De-Morgan 𝓤
                                 → typal-De-Morgan 𝓤
 De-Morgan-gives-typal-De-Morgan {𝓤} fe d A B ν =
  ∣ typal-WEM-gives-untruncated-typal-De-Morgan
     (De-Morgan-gives-typal-WEM fe d)
     A B ν ∣

\end{code}

The above shows that weak excluded middle, De Morgan and truncated De
Morgan are logically equivalent, all in their two (proposional and
typal) versions, so in a total of six logically equivalent statements.

Here is a diagram with the main implications, summarized below in
Agda:

     1 ----> 2
     ^        \
     |         \
     |          \
     |           \
     |            \
     |             \
     |              v
     3 <-- 5 <----- 6
      ^            /
       \          /
        \        /
         \      /
          \    /
           \  v
             4

\begin{code}

 module _ (𝓤 : Universe) where

  private
   ⦅1⦆ = WEM 𝓤
   ⦅2⦆ = typal-WEM 𝓤
   ⦅3⦆ = De-Morgan 𝓤
   ⦅4⦆ = typal-De-Morgan 𝓤
   ⦅5⦆ = untruncated-De-Morgan 𝓤
   ⦅6⦆ = untruncated-typal-De-Morgan 𝓤

  De-Morgan-WEM-diagram
   : funext 𝓤 𝓤₀
   → (⦅1⦆ → ⦅2⦆)
   × (⦅2⦆ → ⦅6⦆)
   × (⦅3⦆ → ⦅1⦆)
   × (⦅4⦆ → ⦅3⦆)
   × (⦅5⦆ → ⦅3⦆)
   × (⦅6⦆ → ⦅4⦆)
   × (⦅6⦆ → ⦅5⦆)
  De-Morgan-WEM-diagram fe =
   WEM-gives-typal-WEM fe ,
   typal-WEM-gives-untruncated-typal-De-Morgan ,
   De-Morgan-gives-WEM fe ,
   typal-De-Morgan-gives-De-Morgan ,
   untruncated-De-Morgan-gives-De-Morgan ,
   untruncated-typal-De-Morgan-gives-typal-De-Morgan ,
   untruncated-typal-De-Morgan-gives-untruncated-De-Morgan

\end{code}

That weak excluded middle and De Morgan are equivalent is long known
and now part of the folklore. We don't know who proved this first,
but, for example, it is in Johnstone's papers on topos theory and his
Elephant two-volume book.

Mike Shulman asked in the HoTT mailing list [1] whether truncated De
Morgan implies untruncated De Morgan, and Martin Escardo offered a proof
as an answer [2], which Mike Shulman added to the nLab [3].

[1] Mike Shulman. de Morgan's Law.
    https://groups.google.com/g/homotopytypetheory/c/Azq6GVU98II/m/qEp8TeInYgAJ
    1st September 2014.

[2] Martin Escardo. de Morgan's Law.
    https://groups.google.com/g/homotopytypetheory/c/Azq6GVU98II/m/bXMixO9s1boJ
    2nd September 2014

[3] Added to the nLab by Mike Shulman.
    https://ncatlab.org/nlab/show/De%20Morgan%20laws.
    2nd September 2014

Here we have added, to both typal-WEM and De Morgan, truncated or not, the
discussion of whether the types in question need to be propositions or
not for them to be all equivalent, and the answer is that it doesn't
matter whether we assume that the types in question are all
propositions.

\begin{code}

 double-negation-is-truncation-gives-DNE : ((X : 𝓤 ̇ ) → ¬¬ X → ∥ X ∥) → DNE 𝓤
 double-negation-is-truncation-gives-DNE f P i u = exit-∥∥ i (f P u)

 non-empty-is-inhabited : EM 𝓤 → {X : 𝓤 ̇ } → ¬¬ X → ∥ X ∥
 non-empty-is-inhabited em {X} φ =
  cases
   (λ (s : ∥ X ∥)
         → s)
   (λ (u : ¬ ∥ X ∥)
         → 𝟘-elim (φ (contrapositive ∣_∣ u))) (em ∥ X ∥ ∥∥-is-prop)

 ¬¬Σ→∃ : {𝓤 𝓣 : Universe} {X : 𝓤 ̇ } → {A : X → 𝓣 ̇ }
       → DNE (𝓤 ⊔ 𝓣)
       → ¬¬ (Σ x ꞉ X , A x )
       → (∃ x ꞉ X , A x)
 ¬¬Σ→∃ {𝓤} {A} {X} {A₁} dn ¬¬Σ = dn _ ∥∥-is-prop (¬¬-functor ∣_∣ ¬¬Σ)

 ∃-not+Π : EM (𝓤 ⊔ 𝓥)
         → {X : 𝓤 ̇ }
         → (A : X → 𝓥 ̇ )
         → ((x : X) → is-prop (A x))
         → (∃ x ꞉ X , ¬ (A x)) + (Π x ꞉ X , A x)
 ∃-not+Π {𝓤} {𝓥} em {X} A is-prop-valued =
  Cases (em (∃ x ꞉ X , ¬ (A x)) ∃-is-prop)
   inl
   (λ (u : ¬ (∃ x ꞉ X , ¬ (A x)))
         → inr (λ (x : X) → EM-gives-DNE
                              (lower-EM (𝓤 ⊔ 𝓥) em)
                              (A x)
                              (is-prop-valued x)
                              (λ (v : ¬ A x) → u ∣ (x , v) ∣)))

 ∃+Π-not : EM (𝓤 ⊔ 𝓥)
         → {X : 𝓤 ̇ }
         → (A : X → 𝓥 ̇ )
         → ((x : X) → is-prop (A x))
         → (∃ x ꞉ X , A x) + (Π x ꞉ X , ¬ (A x))
 ∃+Π-not {𝓤} {𝓥} em {X} A is-prop-valued =
  Cases (em (∃ x ꞉ X , A x) ∃-is-prop)
   inl
   (λ (u : ¬ (∃ x ꞉ X , A x))
         → inr (λ (x : X) (v : A x) → u ∣ x , v ∣))

 not-Π-implies-∃-not : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ }
                     → EM (𝓤 ⊔ 𝓥)
                     → ((x : X) → is-prop (A x))
                     → ¬ ((x : X) → A x)
                     → ∃ x ꞉ X , ¬ A x
 not-Π-implies-∃-not {𝓤} {𝓥} {X} {A} em i f =
  Cases (em E ∃-is-prop)
   id
   (λ (u : ¬ E)
         → 𝟘-elim (f (λ (x : X) → EM-gives-DNE
                                   (lower-EM 𝓤 em)
                                   (A x)
                                   (i x)
                                   (λ (v : ¬ A x) → u ∣ x , v ∣))))
  where
   E = ∃ x ꞉ X , ¬ A x

\end{code}

Added by Tom de Jong in August 2021.

\begin{code}

 not-Π-not-implies-∃ : {X : 𝓤 ̇ } {A : X → 𝓥 ̇ }
                     → EM (𝓤 ⊔ 𝓥)
                     → ¬ ((x : X) → ¬ A x)
                     → ∃ x ꞉ X , A x
 not-Π-not-implies-∃ {𝓤} {𝓥} {X} {A} em f = EM-gives-DNE em (∃ A) ∥∥-is-prop γ
   where
    γ : ¬¬ (∃ A)
    γ g = f (λ x a → g ∣ x , a ∣)

\end{code}

Added by Martin Escardo 26th April 2022.

\begin{code}

Global-Choice' : ∀ 𝓤 → 𝓤 ⁺ ̇
Global-Choice' 𝓤 = (X : 𝓤 ̇ ) → is-nonempty X → X

Global-Choice : ∀ 𝓤 → 𝓤 ⁺ ̇
Global-Choice 𝓤 = (X : 𝓤 ̇ ) → X + is-empty X

Global-Choice-gives-Global-Choice' : Global-Choice 𝓤 → Global-Choice' 𝓤
Global-Choice-gives-Global-Choice' gc X φ = cases id (λ u → 𝟘-elim (φ u)) (gc X)

Global-Choice'-gives-Global-Choice : Global-Choice' 𝓤 → Global-Choice 𝓤
Global-Choice'-gives-Global-Choice gc X = gc (X + ¬ X)
                                             (λ u → u (inr (λ p → u (inl p))))
\end{code}

TODO. Global choice contradicts univalence. This is already present in
the directory MGS.