Judgemental equality

In type theory, judgemental equality or definitional equality is the external notion of equality respected by the type system. While other, internal notions of equality may be defined, judgemental equality is the only kind that the type checker is aware of.

Judgemental equality is usually relied upon when $\mathrm{refl}$ is invoked.