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.

  • $\begingroup$ 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". $\endgroup$ Jun 1, 2020 at 14:41
  • 1
    $\begingroup$ @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. $\endgroup$ Jun 1, 2020 at 15:15
  • $\begingroup$ @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). $\endgroup$
    – Vincent
    Jun 1, 2020 at 15:16


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.