In intuitionistic type theory each type and each well-typed term has a normal form. A consequence of this normal form property is that all the judgments are decidable: for example, given a correct context \(\Gamma\), a correct type \(A\) and a possibly ill-typed term \(a\), there is an algorithm for deciding whether \(\Gamma \vdash a {:} A\). This type-checking algorithm is the key component of proof-assistants for Intensional Type Theory, such as Agda.