Definitional Equality
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:
Judgment | Meaning |
---|---|
a:A | a is an object of type A |
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.
Example are:
- “(λ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.