Quotient types in MLTT imply excluded middle

Quotient.agda

open import Agda.Builtin.Equality

-- Some familiar results about equality

UIP : {A : Set} (x y : A) (p q : x ≡ y) → p ≡ q
UIP x y refl refl = refl

coerce : {A : Set} (B : A → Set)
  → {x y : A} → x ≡ y
  → B x → B y
coerce B refl b = b

infixl 5 _∙_
_∙_ : {A : Set} {a b c : A}
  → a ≡ b → b ≡ c → a ≡ c
refl ∙ refl = refl

sym : {A : Set} {a b : A}
  → a ≡ b → b ≡ a
sym refl = refl

ap : {A B : Set} (f : A → B) {x y : A}
  → x ≡ y → f x ≡ f y
ap f refl = refl

-- Postulate a quotient type

record EquivRel (A : Set) : Set₁ where
  field
    _~_ : A → A → Set
    Refl : ∀ {a} → a ~ a
    Sym : ∀ {a b} → a ~ b → b ~ a
    Trans : ∀ {a b c} → a ~ b → b ~ c → a ~ c

postulate
  _/_ : (A : Set) → EquivRel A → Set

module Quotient {A} (R : EquivRel A) where
  open EquivRel R
  postulate
    [_] : A → A / R
    path : {x y : A} → x ~ y → [ x ] ≡ [ y ]
    sound : {x y : A} → [ x ] ≡ [ y ] → x ~ y
    elim : {M : A / R → Set}  -- Dependent elimination for quotients
      → (f : (a : A) → M [ a ])
      → (∀ x y → (p : x ~ y) → coerce M (path p) (f x) ≡ f y)
      → (x : A / R) → M x

-- We prove the excluded middle

data Bool : Set where true false : Bool
record True : Set where
data False : Set where

true≠false : true ≡ false → False
true≠false ()

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst
open Σ
infixl 1 _,_

module Truncate (P : Set) where
  R : EquivRel Bool
  R = record {
    _~_ = λ { true true → True
            ; true false → P
            ; false true → P
            ; false false → True } ;
    Refl = λ { {true} → _
             ; {false} → _ } ;
    Sym = λ { {true} {true} → _
            ; {true} {false} → λ z → z
            ; {false} {true} → λ z → z
            ; {false} {false} → _ } ;
    Trans = λ { {true} {true} {true} → _
              ; {true} {true} {false} → λ _ z → z
              ; {true} {false} {true} → _
              ; {true} {false} {false} → λ z _ → z
              ; {false} {true} {true} → λ z _ → z
              ; {false} {true} {false} → _
              ; {false} {false} {true} → λ _ z → z
              ; {false} {false} {false} → _ } }

  open EquivRel R
  open Quotient R

  |P| : Set
  |P| = [ true ] ≡ [ false ]

  P→|P| : P → |P|
  P→|P| = path

  |P|→P : |P| → P
  |P|→P = sound

  isProp|P| : (x y : |P|) → x ≡ y
  isProp|P| = UIP _ _

module LEM (P : Set) where
  data Decidable : Set where  -- Datatype recording whether P is true
    yes : P → Decidable
    no : (P → False) → Decidable

  open Truncate P using (R)
  open Quotient R
  open Truncate hiding (R) renaming (|P| to Trunc)

  surj : (x : Bool / R) → Trunc (Σ Bool λ b → x ≡ [ b ])
  surj = elim
    (λ { true → P→|P| _ (true , refl)
      ; false → P→|P| _ (false , refl) })
    λ _ _ _ → isProp|P| _ _ _

  section : (x : Bool / R) → Σ Bool λ b → x ≡ [ b ]
  section x = |P|→P _ (surj x)

  decide : Decidable
  decide with section [ true ] in T | section [ false ] in F
  ... | false , p | y = yes (sound p)
  ... | true , _ | true , p = yes (sound p)
  ... | true , _ | false , _ = no λ p →
    true≠false (sym (ap fst T) ∙ ap (λ b → section b .fst) (path p) ∙ ap fst F)

A comment for my own sake: this shows that postulating quotients of set-valued equivalence relations in MLTT+UIP allows one to define the propositional truncation of a set P as the path type [ true ] ≡ [ false ] in the booleans quotiented by the "suspension" of P. By effectivity one also gets a map ∥P∥ → P, i.e. global choice, from which LEM follows as usual by Diaconescu's theorem.

Postulating effectivity in the stronger form (x ~ y) ≃ ([ x ] ≡ [ y ]) would lead to a contradiction instead, as we would have ∥P∥ ≃ P.