build

{-
`build` is the inverse of `fold`

Examples:

```
./build
(   λ(natural : Type)
→   λ(succ : natural → natural)
→   λ(zero : natural)
→   succ (succ (succ zero))
)
= +3

./build
(   λ(natural : Type)
→   λ(succ : natural → natural)
→   λ(zero : natural)
→   zero
)
= +0
```
-}
let build
    :   (   ∀(natural : Type)
        →   ∀(succ : natural → natural)
        →   ∀(zero : natural)
        →   natural
        )
    →   Natural
    =   Natural/build

in  build