Checking that types adhere to the tying rules.

References: Type theory (nLab)