    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Results concerning the excluded middle axiom.
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Axiom.ExcludedMiddle where

    open import Level using (Level; suc)
    open import Relation.Nullary.Decidable.Core using (Dec)

    ------------------------------------------------------------------------
    -- Definition

    -- The classical statement of excluded middle says that every
    -- statement/set is decidable (i.e. it either holds or it doesn't hold).

    ExcludedMiddle : ∀ ℓ → Set (suc ℓ)
    ExcludedMiddle ℓ = {P : Set ℓ} → Dec P