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?

  • $\begingroup$ They are provably equivalent, and therefore equal as type families. $\endgroup$ – Ptharien's Flame Feb 14 '16 at 1:02
  • 3
    $\begingroup$ I don't think the HoTT book actually defines "homotopy" to mean a path between two proofs of an identity. We intended to only use the word "homotopy" in a precise sense (as opposed to in informal motivating remarks) with the second of your two meanings. Where did you see the first one? $\endgroup$ – Mike Shulman Feb 14 '16 at 6:38
  • 2
    $\begingroup$ @Mike: I think you are right. But for a beginner in this subject it can be quite confusing. I spend some hours trying to find the formal connection between these two uses of the word "homotopy". What makes it even more confusing is the fact that some other papers use the homotopy analogy for proofs of identity types rather extensively. $\endgroup$ – user274886 Feb 14 '16 at 7:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy