Intro to HoTT No. 4, Part 0
In this video, we incorporate into type theory a central feature of logic: implications. Along the way, we encounter the work of the ancient Greek philosopher Theophrastus, the modern work of Brouwer, Heyting, and Kolmogorov, and end up doing computer programming. Quite a journey!
