Type theories usually come with a reduction relation on terms. It computes things like β-reduction for function, inserting arguments into function bodies, compu

Type theories usually come with a reduction relation on terms. It computes things like β-reduction for function, inserting arguments into function bodies, computes projections out of tuples, etc A normal term is one where no further reductions can be made. Without type-in-type you can prove that all terms can be reduced to a normal form. With type-in-type some terms normalise while other diverges. In fact, using type-in-type you can define the fixed point operator and do general recursion!