λ(f : ∀(natural : Type) → (natural → natural) → natural → natural)
→ Natural/build f