AC implies LEM

ACLEM.agda

{-# OPTIONS --safe #-}
module ACLEM where

open import Prelude
open import Meta.Effect
open import Logic.Equivalence
open import Data.Empty
open import Data.Bool
open import Data.Reflects
open import Data.Dec as Dec
open import Data.Sum
open import Data.Quotient.Set

private variable
  ℓ ℓ′ : Level
  
AC : 𝒰ω
AC = ∀ {ℓ ℓ′} {X : Set ℓ} {A : ⌞ X ⌟ → Set ℓ′} 
   → ((x : ⌞ X ⌟) → ∥ ⌞ A x ⌟ ∥₁)
   → ∥ ((x : ⌞ X ⌟) → ⌞ A x ⌟ ) ∥₁

AC→surjsec : AC
           → ∀ {ℓ ℓ′} {X : Set ℓ} {Y : Set ℓ′}
           → (f : ⌞ X ⌟ → ⌞ Y ⌟)
           → is-surjective f
           → ∃[ g ꞉ (⌞ Y ⌟ → ⌞ X ⌟) ] (g section-of f)
AC→surjsec ac {X} {Y} f surj =
  map (λ h → (λ y → fst (h y)) , fun-ext λ y → snd (h y))
      (ac {X = Y} {A = λ z → el! (Σ[ x ꞉ ⌞ X ⌟ ] (f x ＝ z))} surj)

section→injective : {A : 𝒰 ℓ} {B : 𝒰 ℓ′} {f : A → B} {g : B → A}
                  → g section-of f
                  → Injective g
section→injective {f} sec {x} {y} e = happly sec x ⁻¹ ∙ ap f e ∙ happly sec y                          

-- the proof

beq : Prop ℓ → Bool → Bool → 𝒰 ℓ
beq P x y = ⌞ P ⌟ ⊎₁ (x ＝ y)

beq-congr : {P : Prop ℓ} → is-congruence (beq P)
beq-congr {P = P} .is-congruence.equivalence .Equivalence.reflexive .Refl.refl = ∣ inr refl ∣₁
beq-congr {P = P} .is-congruence.equivalence .Equivalence.symmetric Dual.ᵒᵖ = map (map-r _⁻¹)
beq-congr {P = P} .is-congruence.equivalence .Equivalence.transitive .Comp._∙_ p q =
  do p′ ← p
     q′ ← q
     pure ([ inl , (λ x=y → [ inl , (λ y=z → inr (x=y ∙ y=z)) ]ᵤ q′) ]ᵤ p′)
beq-congr {P = P} .is-congruence.has-prop = hlevel!

BQ : Prop ℓ → 𝒰 ℓ
BQ P = Bool / beq P

@0 P≃path : {P : Prop ℓ} → ⌞ P ⌟ ≃ (the (BQ P) ⦋ true ⦌ ＝ ⦋ false ⦌)
P≃path {P} = prop-extₑ! (λ p → ∣ inl p ∣₁) (rec! [ id , false! ]ᵤ) ∙ effective (beq-congr {P = P})

@0 AC→LEM : AC
          → {P : Prop ℓ} → Dec ⌞ P ⌟
AC→LEM ac {P} =
  rec!
    (λ s sec →
      Dec.dmap
        (λ e → P≃path {P = P} ⁻¹ $ section→injective {f = ⦋_⦌} sec e)
        (contra λ p → ap s (P≃path {P = P} $ p))
        (s ⦋ true ⦌ ≟ s ⦋ false ⦌))
    (AC→surjsec (λ {ℓ} {ℓ′} {X} {A} → ac {ℓ} {ℓ′} {X} {A})
                {X = el! Bool} {Y = el! (BQ P)}
                ⦋_⦌ ⦋-⦌-surjective)