Those equalities that are given as rewrite rules (equations) or else originate from general functional principles ( β, η, etc.) - Queiroz, Oliveira.
For 'Homotopy Type Theory' book type theory is a deductive system based on two forms of judgment:
|a:A||a is an object of type A|
|ab : A||a and b are definitionally equal objects of type A|
Definitional equality is a syntactical notion and it has nothing to do with the meaning of the syntactical entries - Nordstrom, Petersson, Smith
Computational (Judgemental) Equality
Equality based on conversion or reduction rules.
- “(λx.x+x)2” and “2+2” (β-reduction)
- “2+2” (s(s(0))+s(s(0)) reduces to “4” (s(s(s(s(0)))).
This is commonly included in definitional equality.