Empty.agda

------------------------------------------------------------------------
-- 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 ()