build

{-
`build` is the inverse of `fold`
-}
let build
    : ( ∀(natural : Type) →
        ∀(succ : natural → natural) →
        ∀(zero : natural) →
          natural
      ) →
        Natural
    = Natural/build

let example0 =
        assert
      :   build
            ( λ(natural : Type) →
              λ(succ : natural → natural) →
              λ(zero : natural) →
                succ (succ (succ zero))
            )
        ≡ 3

let example1 =
        assert
      :   build
            ( λ(natural : Type) →
              λ(succ : natural → natural) →
              λ(zero : natural) →
                zero
            )
        ≡ 0

in  build