∀(natural : Type) → ∀(succ : natural → natural) → ∀(zero : natural) → natural