My friends and I are struggling with understanding intuitively the proof of equivalence between based and free path inductions (HoTT book 1.12.2)

The first major problem is understanding the meaning of the type

page 53

Is there a topological interpretation of this "universal inductor"?

We sort of convinced ourselves that we understand what is going on, but later while reading about path inversion in $\S$ 2.1 it became clear that we don't understand the meaning of this type.

I think that maybe we do not understand the concept of path induction altogether. Our understanding is that to define a function on the path space one needs only the values on constant paths (points) of the space (type). Is this understanding correct?

If someone can give a topological interpretation step-by-step of the first proof for lemma 2.1.1

we will also be very grateful:

page 63

  • 3
    $\begingroup$ This sort of question can only be resolved with interaction. It's extremely difficult to guess which particular thing bothers you. Have you tried talking to people on one of the HoTT forums, like hott.zulipchat.com for example? $\endgroup$ – Andrej Bauer Apr 26 at 21:12
  • $\begingroup$ @AndrejBauer No, I didn't, thank you for the reference! I'll try my luck there then :) $\endgroup$ – Gregory G Apr 26 at 21:53
  • 2
    $\begingroup$ I’m voting to close this question because because of what Andrej said in his comment above. $\endgroup$ – Willie Wong Apr 27 at 3:59