{-
`build` is the inverse of `fold`
-}
let build
    :   ∀(a : Type)
      → (   ∀(optional : Type)
          → ∀(some : a → optional)
          → ∀(none : optional)
          → optional
        )
      → Optional a
    =   λ(a : Type)
      → λ ( build
          :   ∀(optional : Type)
            → ∀(some : a → optional)
            → ∀(none : optional)
            → optional
          )
      → build (Optional a) (λ(x : a) → Some x) (None a)

let example0 =
        assert
      :   build
            Natural
            (   λ(optional : Type)
              → λ(some : Natural → optional)
              → λ(none : optional)
              → some 1
            )
        ≡ Some 1

let example1 =
        assert
      :   build
            Natural
            (   λ(optional : Type)
              → λ(some : Natural → optional)
              → λ(none : optional)
              → none
            )
        ≡ None Natural

in  build