build

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

Examples:

```
./build
Natural
(   λ(optional : Type)
→   λ(just : Natural → optional)
→   λ(nothing : optional)
→   just 1
)
= [ 1 ] : Optional Natural

./build
Natural
(   λ(optional : Type)
→   λ(just : Natural → optional)
→   λ(nothing : optional)
→   nothing
)
= [] : Optional Natural
```
-}
    let build
        :   ∀(a : Type)
          → (   ∀(optional : Type)
              → ∀(just : a → optional)
              → ∀(nothing : optional)
              → optional
            )
          → Optional a
        = Optional/build

in  build