Type Judgement

Definition

A judgment is a metatheoretic assertion concerning the status of constructions within a type theory. Unlike a proposition, which is represented as a type that may or may not be inhabited, a judgment is an absolute statement of fact about the system.

Structure

A judgment is fundamentally contextual. While the core assertion (e.g., $a:A$) denotes a typing relation, it is only formally a judgment when paired with a context $\Gamma$. The turnstile symbol $⊢$ separates the assumptions from the assertion.

Common Judgments

1. $\Gamma ⊢A\text{ type}$: $A$ is a well-formed type in context $\Gamma$.
2. $\Gamma ⊢a:A$: The term $a$ is a valid construction of type $A$ in context $\Gamma$.
3. $\Gamma ⊢a=b:A$: Terms $a$ and $b$ are definitionally equal at type $A$ in context $\Gamma$.
4. $\Gamma \text{ ctx}$: The context $\Gamma$ is well-formed.

References

martin-lof1984-mltt hott2013-book thomson1991-type-theory