Booleans, the original true-false dichotomy

Booleans can have two values, in any given universe. First, we define the Boolean context :

In this context, the type of booleans is simply the .Bool type in context, and the ‘true’ and ‘false’ values are respectively the ‘.true’ and ‘.false’ hypotheses.

We can test that t r u e and f a l s e have the correct type :

  • type of :
  • type of :
  • type of :

Functions on Booleans

Then, we can start defining first-level combinators, such as ‘not’, ‘and’ and ‘or’ :

As always, we should verify the type of our combinators, and test whether they truly conform to their specification :

  • n o t colon upper B o o l e a n right-arrow upper B o o l e a n
  • o r colon upper B o o l e a n right-arrow upper B o o l e a n right-arrow upper B o o l e a n
  • a n d colon upper B o o l e a n right-arrow upper B o o l e a n right-arrow upper B o o l e a n
  • i m p l i e s colon upper B o o l e a n right-arrow upper B o o l e a n right-arrow upper B o o l e a n