13. Equality Types and Proof Relevance

Equality Types and Proof Relevance

Equality types in type theory represent propositions about equality between terms.

In Martin-Löf Type Theory (MLTT), the equality type is usually denoted as eq or =.

Equality types have constructive content, meaning they specify how two terms are equal.

Proof relevance refers to the idea that proofs, or evidence of propositions, are considered as first-class citizens in the type theory.

In MLTT, equality proofs are treated as terms inhabiting the equality type.

This allows reasoning about equality in a formal and constructive manner.

Equality proofs can be generated and manipulated by functions, and they can be pattern matched and analyzed like any other terms.

Lab Activity: Implementing Equality Types and Proof Relevance

Let's implement a simple example in Python to demonstrate equality types and proof relevance.

class EqType:
    def __init__(self, x, y):
        self.x = x
        self.y = y

def refl(x):
    return EqType(x, x)

def main():
    eq_proof = refl(42)
    print("Equality proof:", eq_proof.x, "=", eq_proof.y)

if __name__ == "__main__":
    main()
  

In the lab activity, we define an `EqType` class to represent equality types, which holds two terms x and y.

We then implement the `refl` function, which generates a proof of reflexivity, showing that a term is equal to itself.

We demonstrate the implementation by creating an equality proof for the integer value 42.