{-
`build` is the inverse of `fold`
-}
let build
    :   ∀(a : Type)
      → (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list)
      → List a
    = List/build

let example0 =
        assert
      :   build
            Text
            (   λ(list : Type)
              → λ(cons : Text → list → list)
              → λ(nil : list)
              → cons "ABC" (cons "DEF" nil)
            )
        ≡ [ "ABC", "DEF" ]

let example1 =
        assert
      :   build
            Text
            (   λ(list : Type)
              → λ(cons : Text → list → list)
              → λ(nil : list)
              → nil
            )
        ≡ ([] : List Text)

in  build