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