LEM ≡ ∀ A → A ∨ ¬ A

LEM.agda

module LEM where

open import 1Lab.Type
open import 1Lab.Path
open import 1Lab.HLevel
open import 1Lab.HIT.Truncation
open import Data.Sum

⊥-is-prop : is-prop ⊥
⊥-is-prop ()

LEM : Typeω
LEM = ∀ {ℓ} (A : Type ℓ) → is-prop A → A ⊎ (¬ A)

LEM' : Typeω
LEM' = ∀ {ℓ} (A : Type ℓ) → ∥ A ⊎ (¬ A) ∥

LEM→LEM' : LEM → LEM'
LEM→LEM' lem A = lemma (lem ∥ A ∥ squash)
  where
    lemma : ∀ {ℓ} {A : Type ℓ} → ∥ A ∥ ⊎ ¬ ∥ A ∥ → ∥ A ⊎ (¬ A) ∥
    lemma (inl a) = ∥-∥-rec squash (inc ∘ inl) a
    lemma (inr ¬a) = inc (inr (¬a ∘ inc))

LEM'→LEM : LEM' → LEM
LEM'→LEM lem' A prop = ∥-∥-rec
  (disjoint-⊎-is-prop prop (λ x y i a → ⊥-is-prop (x a) (y a) i) (λ (a , ¬a) → ¬a a))
  id (lem' A)