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
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?
we will also be very grateful: