Intro to HoTT No. 2, Part 0
How do we do Homotopy Type Theory? This is another question with three answers: homotopy type theorists will "dress" their work in three different styles -- informal reasoning, computer formalization, and as inference rules in a deductive system. In these videos, I describe these three styles of HoTT and how a successful homotopy type theorist navigates between them.
