Intro to HoTT No. 1, Part 3
What does homotopy type theory mean? This video presents our third answer: HoTT is a logical calculus for constructively proving statements (especially mathematical claims). This is by way of the famed "Curry-Howard Correspondence", which connects type theory with constructive logic. Along the way, we encounter important notions like proof relevance, unique existence, and (un)inhabitedness. We also go through our first example in Agda, and meet one of the main characters of homotopy type theory: refl.
