I've been reading a lot on type systems and such and I understand roughly why they were introduced (in order to resolve Russel's paradox). I also understand roughly their practical relevance in programming languages and proof systems. However, I'm not entirely confident that my intuitive notion of what a type is, is correct.
My question is, is it valid to claim that types are propositions?
In other words the statement "n is a natural number" corresponds with the statement "n has the type 'natural number'" meaning that all the algebraic rules that involve natural numbers hold for n. (I.e. Said another way, algebraic rules are statements. Those statements that hold true for natural numbers also hold true for n.)
Then does this mean that a mathematical object can have more than one type?
Furthermore, I know that sets are not equivalent to types because you cannot have a set of all sets. Could I claim that if a set is a mathematical object similar to a number or a function, a type is a sort of meta-mathematical object and by the same logic a kind is a meta-meta-mathematical object? (in the sense that every "meta" indicates a higher level of abstraction...)
Does this have some kind of link to category theory?