Import list


module Sets.Indexed where

open import Data.Empty    using (⊥)
open import Data.Unit     using (⊤; tt)
open import Data.Sum      using (_⊎_; inj₁; inj₂)
open import Data.Bool     using (Bool; true; false)
open import Data.Nat      using (ℕ; zero; suc)

Fin, family of finite sets

We wish to define an ℕ-indexed family of sets Fin such that Fin n has exactly n elements.

Given the definition of Fin, the following equivalences would hold:

n Sets with n elements
0 Fin 0 ~ ⊥
1 Fin 1 ~ ⊤ ~ Maybe ⊥ ~ ⊤ ⊎ ⊥
2 Fin 2 ~ Bool ~ Maybe ⊤ ~ Maybe (Maybe ⊥) ~ ⊤ ⊎ ⊤ ⊎ ⊥
3 Fin 3 ~ Maybe Bool ~ Maybe (Maybe (Maybe ⊥)) ~ ⊤ ⊎ ⊤ ⊎ ⊤ ⊎ ⊥
4 Fin 4 ~ Maybe (Maybe (Maybe (Maybe ⊥))) ~ ⊤ ⊎ ⊤ ⊎ ⊤ ⊎ ⊤ ⊎ ⊥
... ...

Definition of Fin

Fin is a set indexed with a natural number (we use Fin because this is not the final definition of Fin):


data Fin : ℕ → Set where
  zero : (n : ℕ) → Fin (suc n)
  suc  : (n : ℕ) → Fin n → Fin (suc n)

The definition yields the statements

zero 0 : Fin 1
zero 1 : Fin 2
zero 2 : Fin 3
...
suc 1 (zero 0) : Fin 2
suc 2 (zero 1) : Fin 3
suc 3 (zero 2) : Fin 4
...
suc 2 (suc 1 (zero 0)) : Fin 3
suc 3 (suc 2 (zero 1)) : Fin 4
suc 4 (suc 3 (zero 2)) : Fin 5
...
...

that could be rearranged as

zero 0 : Fin 1

zero 1 : Fin 2
suc 1 (zero 0) : Fin 2

zero 2 : Fin 3
suc 2 (zero 1) : Fin 3
suc 2 (suc 1 (zero 0)) : Fin 3

zero 3 : Fin 4
suc 3 (zero 2) : Fin 4
suc 3 (suc 2 (zero 1)) : Fin 4
suc 3 (suc 2 (suc 1 (zero 0))) : Fin 4

...

So we can conclude that Fin n has n distinct elements.

Exercises

  1. Define a Bool-indexed family of sets such that the set indexed by false contains no elements and the set indexed by true contains one element.

  2. Define an ℕ-indexed family of sets such that the sets indexed by even numbers contain one element and the others are empty!

Vec A n ~ An

Vec A n is an n-tuple of elements of A:


data Vec (A : Set) : ℕ → Set where
  []   : Vec A zero
  cons : (n : ℕ) → A → Vec A n → Vec A (suc n)

Examples:

[] : Vec ℕ 0
[] : Vec Bool 0
...

cons 0 true [] : Vec Bool 1
...

cons 1 false (cons 0 true []) : Vec Bool 2
...
...

Exercise

Define a Bool-indexed family of sets with two parameters, A and B, such that the set indexed by false contains an A element and the set indexed by true contains a B element.