Import List

module Sets.Recursive where

open import Data.Bool using (Bool; true; false)

The effect of this open import declaration is the same as if we copied the definition of the Bool type here. Note that we enumerated the constructors of Bool too.

More about import declarations will come later.

Peano representation

We are looking for a representation for the natural numbers. The simplest choice is the Peano representation which corresponds to the unary numeral system:

term interpretation in decimal form
zero 0
suc zero 1
suc (suc zero) 2
suc (suc (suc zero)) 3
... ...

Definition of

In Agda, the definition of natural numbers is as follows.

data  : Set where
  zero :     
  suc  :   

Note that this definition yields the infinite set of judgements.

ℕ : Set
zero : ℕ
suc zero : ℕ
suc (suc zero) : ℕ
suc (suc (suc zero)) : ℕ

Type checking of expressions

With the Emacs command C-c C-d, one can get Agda to type check a given expression (d stands for 'deduce').

Example: Hit C-c C-d and enter suc (suc zero).


Deduce the type of the following expressions with Agda:

Binary representation of

Consider the following definition of positive natural numbers, labelled as ℕ⁺:

data ℕ⁺ : Set where
  one      :      ℕ⁺
  double   : ℕ⁺  ℕ⁺
  double+1 : ℕ⁺  ℕ⁺

Note that this definition above yields the following judgements (without ordering):

ℕ⁺ : Set
one : ℕ⁺
double one : ℕ⁺
double+1 one : ℕ⁺
double (double one) : ℕ⁺
double+1 (double one) : ℕ⁺
double (double+1 one) : ℕ⁺
double+1 (double+1 one) : ℕ⁺
double (double (double one)) : ℕ⁺


data ℕ₂ : Set where
  zero :      ℕ₂
  id   : ℕ⁺  ℕ₂


ℕ₂ : Set
zero : ℕ₂
id one : ℕ₂
id (double one) : ℕ₂
id (double+1 one) : ℕ₂
id (double (double one)) : ℕ₂
id (double+1 (double one)) : ℕ₂

Soon we will prove in Agda that and ℕ₂ are isomorphic with the following relation:

zero zero
suc zero id one
suc (suc zero) id (double one)
suc (suc (suc zero)) id (double+1 one)
... ...


  1. How 9 is represented in ℕ₂? Type check that expression.

  2. Why did not we simply use one data definition with 4 constructors, such as zero, one, double, and double+1?

Rationale behind different representations

Each representation has its merit.


Determine which representation ( or ℕ₂) is better for the following tasks.

A good strategy is to choose the right representation for each task and convert values between different representations.


Define .

(Several solutions are possible.)

Binary trees

data BinTree : Set where
  leaf : BinTree
  node : BinTree  BinTree  BinTree


BinTree : Set
leaf : BinTree
node leaf leaf : BinTree
node (node leaf leaf) leaf : BinTree
node leaf (node leaf leaf) : BinTree
node (node leaf leaf) (node leaf leaf) : BinTree

BinTree elements are good for representing binary trees (just the shapes without data).


Define binary trees according to the following shapes.

Binary tree shapes

Binary tree shapes


  1. Define binary trees
  2. Define the lists (finite sequences) of natural numbers.

  3. Define the non-empty lists of natural numbers.