There are different ways of associating interpretations to intuitionistic propositional logic, one of which is to interpret it by Heyting algebras this is the analogue of the standard interpretation of classical logic by Boolean algebras.
Tarski, the On the Concept of Truth in Formal Languages, argued for a properly semantic interpretation of truth, where for example the following sentence:
'p is true' iff p is true
or to give an example in plain English
'Snow is white' iff Snow is white
In both instances the the first sentence is placed in quotes since it should be seen as a purely formal, that is it is built up purely from the grammatical features of the language under consideration.
In this Tarski was considering solely classical logic, and the interpretation is the logical form of the philosophical position of correspondance, where true linguistic propositions correspond to actually true propositions of the world ( the resemblance to model theory here is unmistakable). in the corresponding interpretation of this for intuitionistic logic, the so called BHK interpretation (for Brouwer, Heyting & Kolgomorov), the position is what one might call a constructive position, in that one must supply an account justifying the proposition, that is:
'snow is white' iff Snow is White and this is why...
the formal analogue of this is
'p is true' iff p is provable
One might then associate to the formal proposition all proofs of that proposition. The BHK interpretation also stipulates that each proof is modifiable into another.
Philosophically speaking why should I expect there to be such a mapping? If I have two proofs of a certain proposition why should I expect there to be some means of modifying the first proof into the second?
Presumably this is where homotopy comes in - if we conceive a proof as a path from axioms to the proposition and think of such a modification as a homotopy - a proof that one proof can be modified into another. And then we can carry on further and ask for homotopies between homotopies.
(Homotopy in topology is analytic, in that the paths are built out of points. We could conceive here a proof as analytic in that a proof is built out of propositions linked together via inference rules, but one could take a possibly synthetic approach, I expect, where proofs themselves are basic and not analysable into propositions).
Is this because we can conceive of a proof also as a proposition, or to be more precise, we can see the following as a purely grammatical proposition?
'proof P of p can be modified into a proof Q of p'