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

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

module Axiom.ExcludedMiddle where

open import Level
open import Relation.Nullary

------------------------------------------------------------------------
-- 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 : ( : Level)  Set (suc )
ExcludedMiddle  = {P : Set }  Dec P