In the previous post, we added a parameter to the rational constructor to require the numerator and denominator of rationals to be coprime, in order that we can only construct canonical rationals, so that we get equality that behaves "right" - when two fractions are the same, they will be equal in the eyes of Agda.
But the way we did it doesn't work quite right:
The Curry-Howard correspondence connects propositions and proofs on one side, and datatypes/sets and values/elements of sets on the other side:
|Side A||Side B|
|Programmer view||Maths view|
When we added the coprimality test to the rational constructor, we added a parameter of type
Coprime numerator denominator. That corresponds to the proposition that the numerator and denominator are coprime. Its a parameter so it will have a value when it is used to construct some rational, and that value will be a proof that the numerator and denominator are co-prime.
So now think about constructing a half. We'll put in numerator 1, and denominator 2, and some proof,
Now somebody else builds a half. They'll put in numerator 1, and denominator 2, and some proof,
Now I'm going to compare my half to that other person's half to see if they are equal. They're equal if all the constructor parameters are equal. The numerator, 1, matches. The denominator, 2, matches. But we have a third parameter now, the coprimality proof. Do they match? Does
pr1 = pr2? In general, no, that isn't the case. There could be many different proofs of the same proposition.
So we've ended up with a canonical form for the numerator and denominator, but we've just pushed the problem into a different field of the data structure, and we still don't have a canonical data structure.
Somehow we want to insist that the coprime proposition is true, but without different proofs of that causing different representations of fractions. That is proof irrelevance.
Read on for part IV, the final part