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