Maths - Definitional Equality

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
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.

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.

 

 

 

 

 

EuclideanSpace

home

This Page

This is one of a series of pages about equality in type theory starting on page here.

Terminology

Definitional equality may also be known as:

• Judgemental equality
• External equality

Related Subjects

For more information about Univalence Axiom see page here.

For more information about Propositional, First Order and Higher Order Logic see page here.

Idris Let notation explained here.