Intro to HoTT No. 2, Part 1
How do we do Homotopy Type Theory? In this video, I cover some of the fundamentals of working in Agda (the computer formalization system we'll be using in these videos) and the basic concepts of HoTT as a formal language: judgments, inference rules, formation and introduction.
