Trailing
Richard Eisenberg's blog post I've been triggered to recollect what I have read about the matter so far. Turns out that I was about 17 when I first came into contact with the concept. After my brother hinted to me a month ago that he is reading
"Gödel, Escher, Bach", I grabbed my own copy from my bookshelf and quickly found the page about the fractal nature of provable propositions and the true-false divide. I have scanned it and showing it below.
What is the connection to decidable equality? I believe this illustration shows it:
I have depicted
T (truth, top, any nullary constructor, e.g.
()) at the north pole, and bottom (false, ⊥) at the south pole. The way or reasoning on the north hemisphere is to
transport truth into a type, i.e. construct a function of type
()→P, where
P is the proposition we want to prove in Curry-Howard encoding. As the figure shows we may have a finite number of stops on our way. We can note that a function of type
()→P is isomorphic to
P, so simply constructing an object of type
P suffices.
Dually, proving that a proposition is false, we have to construct a path to bottom from
Q, again possibly via a finite number of stops. Since (
Q→⊥) cannot be simplified we really have to construct functions here.
The equator divides true from false and thus separates the duals.
Since each proof (when computable in finite time) will either result in something from the blue or red island, the type for decidable equality must be
Either (a :~: b) ((a :~: b) -> Void).
