1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.