The Bool set

Consider the definition of Bool with two elements, true and false:

data Bool : Set where
  true  : Bool
  false : Bool


It is due to last two points that the syntax of the definition does not look like that:

Bool  : Set
true  : Bool
false : Bool

Note that:


  1. Define a set named Answer with only three elements: yes, no, and maybe.

  2. Define a set named Direction with only four elements: east, west, north, and south.


Consider the following definition of Bool':

data Bool' : Set where
  true'  : Bool'
  false' : Bool'

  1. Are Bool and Bool' the same sets?

  2. If not, which one is the "real" set of Booleans?


Bool and Bool' are definitionally different but they are isomorphic.

Representation and interpretation

Interpretation (or meaning) is the opposite relation to representation.

Special finite sets

We can define finite sets with n=0,1,2, elements.

The special case with n=0 is the empty set:

data  : Set where   -- Note that there is no constructor at all.

The special case with n=1 is the singleton set (a set with one element):

data  : Set where
  tt : 

and have interesting interpretations as we will see.

Types vs. sets

Basic differences between types and sets:

Thus data defines types, not sets.

Syntactic abbreviation

If we have multiple elements of the same type, it is possible to define them in one line:

data name : Set where
  elem₁ elem₂ : name