Type checking, Hypothetical judgments, meaning explanations and computational type theory
Part of the problem is we cannot say that we have a checker for categorical judgments, because these often reduce to hypothetical judgments. For instance, the categorical judgment $M\in A\to B$ reduces to a hypothetico-general judgment.

In practice, the way that you implement this kind of type theory is by formalizing rules for hypothetico-general equality &amp; membership as a kind of sequent calculus, and then you can write tactics that automate as much of the work as possible. This is the technique used in Nuprl, JonPRL and RedPRL, which all implement type theories of the kind that you describe in your post.