From my understanding, type theory is its own deductive system, meaning that types have propositional meanings. Therefore, an element of a type appears to be an evidence of the truth of the proposition. Likwise, we use the type $0$ (which does not have any element) to disprove propositions by creating functions from one type to $0$.
This model appears to me to classify every proposition to be provable or disprovable depending on whether we can find an element of that type. Thus, it seems to be normal to ask ourselves if type theory would not be a complete consistent theory. Is there any kind of undecidable statements in type theory ? If so, then would it be possible to express it as a type ?