I am learning Homotopy Type Theory with the HoTT book. I am wondering if there are two different definitions of Homotopy there. On the one hand, a homotopy is defined for identity types as a path between two proofs of an identity between two elements. On the other hand, homotopy is also defined between two function types, saying that there is a homotopy between two functions if they are equal elementwise. How are both definitions related?