Judgemental equality

Judgemental equality is equality defined as a judgement, in contrast to propositional or typal equality. The judgements have the form¹

Γ ⊢ 𝐴 = 𝐵, Γ ⊢ 𝑎 = 𝑏 : 𝐴

for “ $𝐴$ and $𝐵$ are judgementally equal (well-typed) types in context $Γ$ ” and “ $𝑎$ and $𝑏$ are judgementally equal (well-typed) terms of (well typed) type $𝐴$ in context $Γ$ ” respectively. Informally, judgemental equality operates at a metatheoretic level: It is proof irrelevant, and cannot be used within the theory e.g. as the antecedent of a conditional. The actual meaning of judgemental equality depends on the type theory used

In intensional type theories like ITT, judgemental equality may be viewed as definitional equality, syntactic equality, or intensional equality. Types or terms are judgementally equal if they have precisely the same sense, as in the Sense and denotation.
In extensional type theories like ETT, judgemental equality reflects propositional/typal equality (given by the Extensional equality type).

Usual inference rules

Both sides of a type equality judgement are themselves types:

Γ ⊢ 𝐴 = 𝐵 Γ ⊢ 𝐴 Γ ⊢ 𝐴 = 𝐵 Γ ⊢ 𝐵

Similarly, both sides of a term equality judgement are themselves terms:

Γ ⊢ 𝑎 = 𝑏 : 𝐴 Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑎 = 𝑏 : 𝐴 Γ ⊢ 𝑏 : 𝐴

Judgemental equality of types is an equivalence relation

Γ ⊢ 𝐴 Γ ⊢ 𝐴 = 𝐴 Γ ⊢ 𝐴 = 𝐵 Γ ⊢ 𝐵 = 𝐴 Γ ⊢ 𝐴 = 𝐵 Γ ⊢ 𝐵 = 𝐶 Γ ⊢ 𝐴 = 𝐶

and likewise for terms

Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑎 = 𝑎 : 𝐴 Γ ⊢ 𝑎 = 𝑏 : 𝐴 Γ ⊢ 𝑏 = 𝑎 : 𝐴 Γ ⊢ 𝑎 = 𝑏 : 𝐴 Γ ⊢ 𝑏 = 𝑐 : 𝐴 Γ ⊢ 𝑎 = 𝑐 : 𝐴 .

We have the variable conversion rule, for a generic judgement thesis $J$

Γ ⊢ 𝐴 = 𝐴' Γ, 𝐴, Δ ⊢ J Γ, 𝐴', Δ ⊢ J (V)

which guarantees Indiscernibility of identicals for types. Finally, judgemental equality is a “congruence” with respect to substitution:

Γ ⊢ 𝑎 = 𝑎' : 𝐴 Γ, 𝑥 : 𝐴, Δ ⊢ 𝐵 Γ, Δ [𝑎 / 𝑥] ⊢ 𝐵 [𝑎 / 𝑥] = 𝐵 [𝑎' / 𝑥] (T V =) Γ ⊢ 𝑎 = 𝑎' : 𝐴 Γ, 𝑥 : 𝐴, Δ ⊢ 𝑡 : 𝐵 Γ, Δ [𝑎 / 𝑥] ⊢ 𝑡 [𝑎 / 𝑥] = 𝑡 [𝑎' / 𝑥] : 𝐵 [𝑎 / 𝑥] (t V =)

Further inference rules on judgemental equality are given for individual types in the type theory, and are often classified under α-conversion, $𝛽$ -computation, and η-reduction.² #m/def/type

#state/tidy | #lang/en | #SemBr

We depart from the usual convention: Type-theoretic literature will usually reserve $(=)$ for typal equality, using either $(\equiv)$ or $(˙ =)$ for judgemental equality. We take the opposite approach, which is more akin to the notation used in proof assistants. This is also used in Principles of dependent type theory. ↩
2025. Introduction to Homotopy Type Theory, §1, pp. 11–19 ↩

Judgemental equality

Usual inference rules

Footnotes