My question is related to the formal presentation of type theory as stated in the context of Homotopy Type Theory. Every formalization is grounded on typing judgements like $$ a: A $$ where mostly it is said that $a$ is an object that can be built due to several formation or term-forming rules and $A$ is a Type. But are types and objects different layers or is every type in some sense also a term. So in conclusion: Is there only one base class of mathematical entities in general?
I'm aware that the objects above are proofs. What confuses me mostly is that for the universe hierarchy postulated one has $$ U_n : U_m $$ for $n<m$. Statements of the form $$A : B$$ with $A$ and $B$ types suggest me to believe that there is no distinction between proofs and Types. Is this the correct point of view?
Addendum, 01.01.2015: I think the "homotopy perspective" is also a clue for that - if one assumes that points of a space can be regarded as spaces itself in some sense.
I have found a very nice answer on CS SE. Roughly spoken the answer is: Depending on the type theory used, there is no distinction (or there is). To quote the answer there:
There are type systems that go further and completely mix types and base terms, so that there is no distinction between the two. Such type systems are said to be higher-order.
So my question reduces to: Is it true that in Martin-Löf Type Theory, which HoTT is based on, there is no distinction between terms and types?