------------------------------------------------------------------------
-- The Agda standard library
--
-- Empty type, judgementally proof irrelevant, Level-monomorphic
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Data.Empty where
 
open import Data.Irrelevant using (Irrelevant)
 
------------------------------------------------------------------------
-- Definition
 
-- Note that by default the empty type is not universe polymorphic as it
-- often results in unsolved metas. See `Data.Empty.Polymorphic` for a
-- universe polymorphic variant.
 
private
  data Empty : Set where
 
-- ⊥ is defined via Data.Irrelevant (a record with a single irrelevant
-- field) so that Agda can judgementally declare that all proofs of ⊥
-- are equal to each other. In particular this means that all functions
-- returning a proof of ⊥ are equal.
 
⊥ : Set
⊥ = Irrelevant Empty
 
{-# DISPLAY Irrelevant Empty = ⊥ #-}
 
------------------------------------------------------------------------
-- Functions
 
⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
⊥-elim ()
 
⊥-elim-irr : ∀ {w} {Whatever : Set w} → .⊥ → Whatever
⊥-elim-irr ()