lo.logic - When are two proofs of the same theorem really different proofs

Some additional recent references on "equivalence" or "homotopy" between proofs include

1) S. Awodey, Type theory and homotopy, also on the arXiv

2) Various notes by V. Voevodsky

Not that I understand much of these - certainly not much enough to see a down-to-earth example of two explicit proofs of some elementary statement that are not homotopic, as detected by some invariant. Is anyone able to provide such an example?

3) J. Conant and O. Thistlethwaite, Boolean formulae, hypergraphs and combinatorial topology

Then, there are two very basic things to note. First, the question itself dates back to Hilbert's (would-be) 24th Problem, which R. Thiele discovered in Hilbert's notebooks a century later (translation and remarks by Thiele, boldface mine):

The 24th problem in my Paris lecture was to be: Criteria of simplicity, or proof
of the greatest simplicity of certain proofs. Develop a theory of the method of
proof in mathematics in general. Under a given set of conditions there can be but
one simplest proof. Quite generally, if there are two proofs for a theorem, you
must keep going until you have derived each from the other, or until it becomes
quite evident what variant conditions (and aids) have been used in the two proofs.
Given two routes, it is not right to take either of these two or to look for a third;
it is necessary to investigate the area lying between the two routes. Attempts at
judging the simplicity of a proof are in my examination of syzygies and syzygies
between syzygies. The use or the knowledge of a syzygy simplifies in an
essential way a proof that a certain identity is true. Because any process of addition [is] an application of the commutative law of addition etc. [and because]
this always corresponds to geometric theorems or logical conclusions, one can
count these [processes], and, for instance, in proving certain theorems of elementary geometry (the Pythagoras theorem, [theorems] on remarkable points of
triangles), one can very well decide which of the proofs is the simplest. [Part of the last sentence is not only barely legible in Hilbert’s notebook but also grammatically incorrect. Corrections and insertions that Hilbert made in this entry show that he wrote down the problem in haste.]

Second, there is a good reason why the question has been traditionally treated in an intuitionistic setup, from Seely to Awodey. (Note that intuitionistic proofs are perhaps less scary if thought of as computer programs, via the Curry-Howard correspondence.) The reason is that in classical logic, with a standard formalization of the notion of "proof", every two proofs of the same statement must be equivalent with every reasonable notion of equivalence. The idea is in Kevin Buzzard's answer. For a rigorous explanation see Yves Lafont's Appendix B in Girard's Proofs and Types (The standard sequent calculus notation used in that appendix is introduced in the very beginning of the book.) It looks like Alessio Guglielmi has some way of overcoming this difficulty by using a non-standard proof-theoretic setup which I wish I understood better.