The Empty Type
Table of Contents
1 Empty
module Lib.Data.Empty where
This file defines the empty type, i.e., the type that is not inhabited. It provides its (degenerate) induction principle together with the very useful ex-falso. It also defines the negation, that is, the emptiness of a type.
1.1 Definition
data Empty : U =
1.2 Induction principle
ind-Empty (P : Empty → U) : (x : Empty) → P x = split
ex-falso is actually a special case of the induction principle.
ex-falso (A : U) : Empty → A = ind-Empty (λ_. A)
1.3 Negation
The negation on a type A is a proof that A is not inhabited.
neg (A : U) : U = A → Empty
1.4 Emptiness
A type is empty if it is not inhabited. The function is-empty is a semantic shortcut for neg.
is-empty (A : U) : U = neg A