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