`Bool`

setConsider the definition of `Bool`

with two elements, `true`

and `false`

:

data Bool : Set where true : Bool false : Bool

*Interpretation:*

`Bool`

is a`Set`

.`true`

is a`Bool`

.`false`

is a`Bool`

.- There is
*nothing else*that is`Bool`

. `true`

and`false`

are different values.

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

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'

Are

`Bool`

and`Bool'`

the same sets?If not, which one is the "real" set of Booleans?

`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