The Different Types of Equality

the_different_types_of_equality.md

The Different Types of Equality

I don't have much to say about this topic since I don't fully understand it.

Basically here are the types of equality I've found:

• Axiomatic
• Defined
• Identity
• Intensional Equality - [[1,2],[3,4]] == [[1,2],[3,4]] or Just 1 == Just 1
• Definitional Equality - 2 == s(s(z)) or T :: Type or t : T
• Extensional Equality - (\x -> x + 1) == (\y -> 1 + y)
• Computational Equality - (\x -> x + x) 2 == 2 + 2 or 2 + 2 == 4
• Propositional Equality - a + b == b + a
• Isomorphism
• Equivalence
• Congruence
• Univalence

They can all mean slightly different things in different theoretical contexts.

See:

• https://ncatlab.org/nlab/show/equality
• http://kodu.ut.ee/~varmo/tday-andu/chapman-slides.pdf
• http://www.uff.br/ebl/slides/contributions/ruy_de_queiroz.pdf
• http://adam.chlipala.net/cpdt/html/Equality.html
• http://jozefg.bitbucket.org/posts/2014-08-06-equality.html
• http://wisnesky.net/ext.pdf
• https://en.wikipedia.org/wiki/Equality_%28mathematics%29

Intensional Equality

In Haskell, intentional equality is expressed with the Eq typeclass. Any term with the same constructors, and same terms, and the same number of each is intentionally equal.

For functions, intensional equality would mean that the functions have the same source code. Does this mean syntactic equality? What about code-transformation? Who knows? Do we consider bit-level equality to be equal if the bits are designed for 2 different interpreters?

I still think this is contextual to some extent.

This equality can also be applied to the type level.

It is interesting to note that newtype wrappers and the type they have wrapped is not intensionally equal, but to some perspective, they can be considered extensionally equal.

Extensional Equality

This is behavioural equality. Generally applied to functions. 2 functions are extensionally equal if the functions have the exact same domain and image. Remember that the "image" of a function is the subset of the co-domain, it represents the values that can actually returned from the function, not every possible value of the co-domain. I think this also means the domain must be equally total or equally partial. One function that is total is not extensionally equal to another function which is partial.

Univalence

Something to do with isomorphisms? And figuring out equalities between proofs, and equalities between equality proofs.

Isomorphism

In Category Theory, equality is generally considered up to isomorphism. This means can say that {1, 2, 3} and {Red, Green, Blue} are equal up to isomorphism. An isomorphism is simply that there reversible morphisms that map from one object to another. That is, you can define a morphism {1, 2, 3} -> {Red, Green, Blue} and {Red, Green, Blue} -> {1, 2, 3}. In fact such a mapping operation is a simple substitution, with the map being directly encoded in the morphic function.

My opinion is that the word "equality" is quite ambiguous and relies on context to understand what it means. When comparing 2 very complex things, a statement which states that the 2 are equal, often requires caveats and extra explanation, as to what it considers equality to be in the situation presented.

Two things are the same (in HoTT and elsewhere) when one can be substituted for the other in any context. https://www.reddit.com/r/math/comments/1wzgyn/why_does_voevodskys_univalence_axiom_imply_that/

That's an interesting notion. We could say "same" is the strongest level of equality, where if 2 things can be substituted for each other in ANY context at all, and nothing would change, then the 2 things are the same.

If any situation where the 2 things cannot be substituted for each other in ANY context, but only PARTICULAR contexts, then we cannot have such a strong level of equality.