[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] ## In type theory ### Definitional equality Another notion is _definitional equality_ or _intensional equality_. According to [PML (1980), p. 31](#PML): > Definitional equality is intensional equality, or equality of meaning (synonymy). [...] It is a relation between linguistic expressions [...] Definitional equality is the equivalence relation generated by abbreviatory definitions, changes of [[bound variables]] and the [[principle of substituting equals for equals]]. [...] Definitional equality can be used to rewrite expressions [...]. on p. 60: > ... intensional (sameness of meaning) ... For instance the symbols "$2$" and "$s(s(0))$" (meaning the successor of the successor of $0$) are definitionally/intensionally equal terms (of type the [[natural numbers]]): the first is merely an abbreviation for the second. category: redirected to nlab