Definition. Empty Type [hca/H002.lagda]

The simplest type we can define in agda is the empty type.

data 𝟘 : Type where

Since we are giving no way to introduce it, it has no elements. Because we can be sure to never encounter an element x : 𝟘, we assume an elimination rule that gives us an element of any type A given x : 𝟘.

postulate
  A : Type

explosion : 𝟘 -> A
explosion ()