Type theory MOC

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 typal equality.

The judgemental equality for types as presented here is limited to dependent type theories.

Standard 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:

Γ⊢𝑎=𝑎′:𝐴Γ,𝑥:𝐴,Δ⊢𝐵Γ,Δ[𝑎/𝑥]⊢𝐵[𝑎/𝑥]=𝐵[𝑎′/𝑥](TV=)Γ⊢𝑎=𝑎′:𝐴Γ,𝑥:𝐴,Δ⊢𝑡:𝐵Γ,Δ[𝑎/𝑥]⊢𝑡[𝑎/𝑥]=𝑡[𝑎′/𝑥]:𝐵[𝑎/𝑥](tV=)

Further inference rules on judgemental equality are given for individual types in the type theory, and are often classified under α-conversion, β-reduction, and η-reduction.² type

Properties

1. The element conversion rule

Γ⊢𝐴=𝐴′Γ⊢𝑎:𝐴Γ⊢𝑎:𝐴′ (E)

is derivable. ^P1 2. The congruence rule for element conversion

Γ⊢𝐴=𝐴′Γ⊢𝑎=𝑎′:𝐴Γ⊢𝑎=𝑎′:𝐴′ (E=)

is derivable.

Proof

We give the formal deduction

Γ⊢𝑎:𝐴Γ⊢𝐴=𝐴′Γ⊢𝐴′=𝐴Γ⊢𝐴=𝐴′Γ⊢𝐴′Γ,𝑥:𝐴′⊢𝑥:𝐴′(𝛿)Γ,𝑥:𝐴⊢𝑥:𝐴′(V)Γ⊢𝑎:𝐴′(S)

proving ^P1.

Similarly,

Γ⊢𝑎=𝑎′:𝐴Γ⊢𝐴=𝐴′Γ⊢𝐴′=𝐴Γ⊢𝐴=𝐴′Γ⊢𝐴′Γ,𝑥:𝐴′⊢𝑥:𝐴′(𝛿)Γ,𝑥:𝐴⊢𝑥:𝐴′(V)Γ⊢𝑎=𝑎′:𝐴′(tV=)

proving ^P2.

---

tidy | en | SemBr

Footnotes

1. We depart from the usual convention: Type-theoretic literature will usually reserve ( =) for typal equality, using either ( ≡) 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 @angiuliPrinciplesDependentType2025. ↩

2. 2025. Introduction to Homotopy Type Theory, §1, pp. 11–19 ↩