Boolean algebra is a branch of mathematics dealing with formalized logic, and is closest to the programmerâ€™s daily toolbox than any other branch of mathematics, except, say, arithmetic. Our computing infrastructure is built around binary values, and hence, computing systems are essentially compound machines consisting of simpler uints that perform logical operations, think digital gates and circuits. In fact, the invention of logic gates that essentially ushered this new era of computing that we assume the reader to be familiar with.

We try to formally state the system of Logic and its mathematical machinery, consisting of various relations, transformations and laws using the language of Type Theory represented by Agda. We begin with the basics of logic - its objects and operations on those objects, then move on to constructively proving the laws of Boolean algebra. In doing this, we also intend to provide a basic intoduction on how a branch of mathematics can be formalized in Agda.