Library HoTT.ExcludedMiddle

Require Import HoTT.Basics HoTT.Types.

The law of excluded middle


Monomorphic Axiom ExcludedMiddle : Type0.
Existing Class ExcludedMiddle.

Mark this axiom as a "global axiom", which some of our tactics will automatically handle.
Global Instance is_global_axiom_excludedmiddle : IsGlobalAxiom ExcludedMiddle := {}.

Axiom LEM : ∀ `{ExcludedMiddle} (P : Type), IsHProp P → P + ¬P.

Definition ExcludedMiddle_type := ∀ (P : Type), IsHProp P → P + ¬P.

LEM means that all propositions are decidable


Global Instance decidable_lem `{ExcludedMiddle} (P : Type) `{IsHProp P} : Decidable P
  := LEM P _.

Double-negation elimination


Definition DNE_type := ∀ P, IsHProp P → ~~P → P.

Definition LEM_to_DNE : ExcludedMiddle → DNE_type.
Proof.
  intros lem P hp nnp.
  case (LEM P _).
  - auto.
  - intros np; elim (nnp np).
Defined.

This direction requires Funext.
Definition DNE_to_LEM `{Funext} :
  DNE_type → ExcludedMiddle_type.
Proof.
  intros dn P hp.
  refine (dn (P + ¬P) _ _).
  - apply ishprop_sum.
    + exact _.
    + exact _.
    + intros p np; exact (np p).
  - intros nlem.
    apply nlem.
    apply inr.
    intros p.
    apply nlem.
    apply inl.
    apply p.
Defined.

DNE is equivalent to "every proposition is a negation".
Definition allneg_from_DNE (H : DNE_type) (P : Type) `{IsHProp P}
  : {Q : Type & P ↔ ¬Q}.
Proof.
  ∃ (¬P); split.
  - intros p np; exact (np p).
  - apply H; exact _.
Defined.

Definition DNE_from_allneg (H : ∀ P, IsHProp P → {Q : Type & P ↔ ¬Q})
  : DNE_type.
Proof.
  intros P ? nnp.
  destruct (H P _) as [Q e].
  apply e.
  intros q.
  apply nnp.
  intros p.
  exact (fst e p q).
Defined.