# 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". – Andrej Bauer 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. – jmite 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). – Vincent Jun 1 '20 at 15:16