# Natural numbers as types.

My question could be simple but I haven't found an answer for it: could we define a type theory where the types are the natural numbers themselves (not the set of the natural numbers)?

Thanks.

-
what exactly do you mean by type theory? – Ittay Weiss Jan 7 '13 at 10:56
I mean an Intuitionistic type theory or constructive type theory. – Gibarian Jan 7 '13 at 11:02
Do you mean something like the theory of simple types (TST)? – Zhen Lin Jan 7 '13 at 11:26
Ah, yes, thanks. I hadn't any idea about it. – Gibarian Jan 7 '13 at 11:53

Most type system will have 1 or True the type with a single unique in habitant.