Booleans in HoTT: Boolean Combinators

Description

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! This video shows how to recreate the logic of boolean circuits and logic gates, both in informal HoTT and in our Agda formalization of HoTT.

Formalization links:

• The formalization I’m developing for this video series

HoTT textbooks:

• The HoTT Book (2013)—the original statement of HoTT
• Introduction to Homotopy Type Theory, by Egbert Rijke (to be released)