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