The type system of intuitionistic type theory is very expressive. As a consequence the well-formedness of a type is no longer a simple matter of parsing, it is something which needs to be proved. Well-formedness of a type is one form of judgment of intuitionistic type theory. Well-typedness of a term with respect to a type is another. Furthermore, there are equality judgments for types and terms. This is yet another way in which intuitionistic type theory differs from ordinary first order logic with its focus on the sole judgment expressing the truth of a proposition.