```agda
module Data.Fin where

open import Data.Fin.Properties public
open import Data.Fin.Finite public
open import Data.Fin.Base public
```

# Finite sets - index

The natural numbers are constructed in the module
[`Data.Fin.Base`]. Their arithmetical properties are proved in
[`Data.Fin.Properties`].

[`Data.Fin.Base`]: Data.Fin.Base.html
[`Data.Fin.Properties`]: Data.Fin.Properties.html
