Intro to HoTT No. 3, Part 1
Boolean logic is an important part of computer science, both at the hardware level and the software level. Can we do boolean logic in HoTT? Of course we can! In this video, I give our first example of the iteration and computation rules for a type, which are how we use types. With booleans, this corresponds to gate-like constructs called multiplexers and to the ubiquitous 'if-then-else' construction of programming languages.
