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
a=b : 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:

This is commonly included in definitional equality.






metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.


Terminology and Notation

Specific to this page here:


This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2022 Martin John Baker - All rights reserved - privacy policy.