Are types propositions? (What are types exactly?)
The key role of types is to partition the objects of interest into different universes, rather than considering everything existing in one universe. Originally, types were devised to avoid paradoxes, but as you know, they have many other applications. Types give a way of classifying or stratifying objects (see blog entry).

Some work with the slogan that propositions are types, so your intuition certainly serves you well, though there is work such as Propositions as [Types] by Steve Awodey and Andrej Bauer that argues otherwise, namely that each type has an associated proposition. The distinction is made because types have computational content, whereas propositions don't. 

An object can have more than one type due to subtyping and via type coercions.

Types are generally organised in a hierarchy, where kinds play the role of the type of types, but I wouldn't go as far as saying that types are meta-mathematical. Everything is going on at the same level – this is especially the case when dealing with dependent types.

There is a very strong link between types and category theory. Indeed, Bob Harper (quoting Lambek) says that Logics, Languages (where types reside), and Categories form a holy trinity. Quoting:


  These three aspects give rise to three sects of worship: Logic, which gives primacy to proofs and propositions; Languages, which gives primacy to programs and types; Categories, which gives primacy to mappings and structures. 


You should look at the Curry-Howard Correspondence to see the link between Logic and Programming Languages (types are propositions), and Cartesian Closed Categories, to see the between the relationship with Category Theory.