What is the difference between judgmental equality, definitional equality, and equality types?

Question

This answer to this question about η-equivalence in Coq draws a distinction between judgmental equality and definitional equality.

In the simply typed lambda calculus (henceforth STLC), the following is an example of a typing rule.

$$ \frac{\Gamma \vdash t_1 : \alpha \to \beta \;\; \text{and} \;\; \Gamma \vdash t_2 : \alpha}{\Gamma \vdash t_1(t_2) : \beta } \;\; \text{is modus ponens} $$

In my understanding, $t_1 : \alpha \to \beta$ is a typing judgment.

STLC can be formalized using typing judgments exclusively.

Judgmental equality is slightly more confusing.

Does it refer to a new type of judgment such as $t_1 = t_2$ for terms and $\alpha_1 = \alpha_2$ for types, as described here?

I think an equality type is just a type $t_3 : \alpha \equiv \beta$ that can be inhabited or not like any other type.

Assuming the above is true, then, I'm not sure what definitional equality would be.

Answer 1

This answer to this question about η-equivalence in Coq draws a distinction between judgmental equality and definitional equality.

This is an incorrect attribute to the answer you linked to. Sarah didn't say that judgmental equality is distinct from definitional equality. I suggest reading that answer again.

Judgmental equality usually means the fact that two terms are semantically exactly the same (in other words, they share the same "semantical object"). Definitional equality is a synonym of judgmental equality.

Equality types are types that encode certain equality, or "witness" certain equality. Usually, an equality type is parameterized by two terms (and maybe something else), where every instance of such type is a proof that these two terms satisfy an equality. Equality relations encoded in an equality type are usually called "propositional equality". There can be different equality relations encoded by different equality types, depending on the exact definition of the equality types. In my impression, they're mostly stronger than the mathematical sense of equivalence relation (binary relation that is refl, sym, and trans).

Obviously, judgmental equality implies propositional equality (check!), but the reverse direction is not true. In case the reverse is true, we usually refer to the type theory as an extensional type theory, with the reverse known as 'equality reflection'.

Answer 2

Nick de Bruijn invented the distinction between "definitional equality" and "book equality" in:

• Bruijn, de, N. G. (1975). Set theory with type restrictions. In A. Hajnal, R. Rado, & V. T. Sos (Eds.), Infinite and finite sets : to Paul Erdõs on his 60th birthday, vol.1 (pp. 205-214). (Colloquia Mathematica Societatis János Bolyai; Vol. 10). North-Holland Publishing Company. Eprint

Basically, two terms (or two types) are "definitional equivalent" $t_{1}=_{d}t_{2}$ if they can be transformed into the same term $t$ by definitional expansion, beta reduction, and eta expansion.

Book equality, or propositional equality, is a type $eq(-,-)$ parametrized by two terms of the same type $t_{1} : A$, $t_{2} : A$, satisfying the familiar identities of equality (reflexivity, transitivity, etc.). Usually this is the equality you're thinking of in mathematics.

See also:

• Thierry Coquand, Nils Anders Danielsson, "Isomorphism is Equality" Eprint