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

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

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

Properties

1. The element conversion rule

is derivable. 2. The congruence rule for element conversion

is derivable.

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