# Summary of types of equivalence and equality in type theory, with notations and examples

Coming from non-computer science background, I am trying to understand the different types of equivalence and equality usually used in type theory. Ideally, I am looking for clear definitions and notations (ie the symbols commonly used) of:

• difference between equivalence and equality of types $$T_{1}$$ and $$T_{2}$$
• definitional equivalence(/equality?) of types $$T_{1}$$ and $$T_{2}$$
• structural equivalence(/equality?) of types $$T_{1}$$ and $$T_{2}$$
• observational equivalence(/equality?) of types $$T_{1}$$ and $$T_{2}$$
• denotational equivalence(/equality?) of types $$T_{1}$$ and $$T_{2}$$
• [other] equivalence(/equality?) of types $$T_{1}$$ and $$T_{2}$$
• etc...

Illustrations of the different types of equivalence/equality in a common programming language (ideally C++) would also really help.

• The terminology varies and so it's difficult to give you a good answer, unless you tell us what your sources were. Where did you see these terms used, specifically? For example, "boservational equivalence" can mean several things, and so can "equivalence". Jun 1 '20 at 14:41
• @Vincent You're also not likely to see good examples of these in C++, because many of these are concepts that specifically apply to dependently-typed languages, which C++ is not. Jun 1 '20 at 15:15
• @AndrejBauer I could not really pinpoint where I saw each of these, I just know I've seen them in type theory books. If you have the knowledge to answer the question from the standpoint of a particular domain/community/author, that would already be a big help. I posted this question a while ago and back at that time, I was reading books on type theory and HoTT. (and you can forget the illustration part, I think I've read enough on type theory now to be able to interpret your answer). Jun 1 '20 at 15:16