Definition 1.2.1.  We define:
Bool :=: {[p] | p is a proposition}
[p] = [q]  :⇔  [p  ⇔  q]  (p is a proposition, q is a proposition)
Remarks.

This definition captures propositions up to equivalence. Since HLM uses classical logic, it can be proved to contain only two values, true and false. It can therefore be used interchangeably with the set $../Numbers/Natural/Subsets/"Binary digits" of binary digits.

References.