The `Bool` set

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


data Bool : Set where
  true  : Bool
  false : Bool

Interpretation:

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:

The data and the where are keywords.
The Set is the set of sets (a constant).
The ':' is pronounced "is a" or "type of", it has similar rule as '∈' in set theory. We do not use the '∈' symbol because ':' and '∈' have different meanings which will be discussed in details later.
Indentation matters.
Spaces matter.
We call true and false constructors of the data type Bool (more explanation on constructors will come later).

Exercises

Define a set named Answer with only three elements: yes, no, and maybe.
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'

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

Two sets are isomorphic if there is a one-to-one relation between their elements.
We will represent isomorphisms in Agda later.

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

The interpretation (the meaning) of Bool is the set of Boolean values.
One possible representation of the set of Booleans is Bool.
Another possible representation of the set of Booleans is Bool'.
Different interpretations of the same definition are also possible as we will see.

We can define finite sets with $n = 0, 1, 2, \dots$ 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.

Basic differences between types and sets:

The type of an element is unique ↔ an element can be member of different sets. E.g. true cannot be the element of two different types at the same time.
A type is not just the collection of its elements ↔ a set is characterized by its elements. E.g. there are different empty types.

Thus data defines types, not sets.

We prefer types over sets for several reasons.
From now on, we use both terms "type" and "set" for types. We use the term "element" for types too.
Set is the type of types, so it should be called Type. However, Agda 2.3.2 and before (and probably after too) calls it Set.
Agda makes it possible to give the same name to the constructors of different types -- but only if each constructor application remains unambiguous that way.

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