Hacker News Reader

Comment by zingermc | Hacker News Reader

That was making my eyes cross, so I drew it out. In short, there are two distinct paths that you can apply a transitive rule over to get A -> D.

Very cool example!

View on HN

It can get more complicated. When your logic can talk about equivalence of equivalences of proofs, then you can have two proofs that are equivalent in two ways that are not equivalent. Or, you could have two proofs that are equivalent in two ways whose equivalence can be proved, but maybe also in more than one way. You can iterate equivalences of equivalences in such a logic and equality becomes a significantly richer concept.

The study of such mathematical structures is the study of what is called an (infinity,1)-topos.

For readers who aren't already familiar with this, I'll note that this is in large part what Homotopy Type Theory is about making easy to work with. http://homotopytypetheory.org/book/ is a good introduction.

One could argue that the proof is just that all As are Xs where all Xs are Ds and therefore all As are Ds. This factors out the detail of choosing one path over the other. You have of course still to show that such an X exists and can use either pair of the axioms establishing this but as far as this proof is concerned both axiom pairs are really equivalent. So are this really two different proofs? How would one define equivalence between proofs to begin with? Isomorphic graphs of applied derivation rules?

Reply on news.ycombinator.com