A definition for finite sets in Agda

Question

I am new to Agda. I'm reading the paper "Dependent Types at Work" by Ana Bove and Peter Dybjer. I don't understand the discussion of Finite Sets (on page 15 in my copy).

The paper defines a Fin type:

data Fin : Nat -> Set where
    fzero : {n : Nat} -> Fin (succ n)
    fsucc : {n : Nat} -> Fin n -> Fin (succ n)

I must be missing something obvious. I don't understand how this definition works. Could someone simply translate the definition of Fin into everyday English? That might be all I need to understand this part of the paper.

Thanks for taking the time to read my question. I appreciate it.

Answer 1

data Fin : Nat -> Set where

Fin is a data type parametrized by a natural number (or: Fin is a type-level function which takes a Nat and returns a Set (basic type), i.e. for any natural number n Fin n is a Set).

    fzero : {n : Nat} -> Fin (succ n)

For all natural numbers n fzero is a member of the type/set Fin (succ n), from which follows that for all positive numbers n (i.e. all naturals except zero), fzero is a member of Fin n.

    fsucc : {n : Nat} -> Fin n -> Fin (succ n)

For all natural numbers n and all values m of type Fin n, fsucc m is a member of type Fin (succ n).

---

So fzero is a member of Fin n for all n except zero and fsucc m is a member of Fin n for all n which represent a number greater than fsucc m.

Basically Fin n represents the Set of all natural numbers smaller than n, i.e. of all valid indices for lists of size n.