3
$\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.

Improve this question
$\endgroup$
3
  • $\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$
    – Andrej Bauer
    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$
    – jmite
    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

0

Reset to default

Your Answer

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