Note that `false` the value of type `Bool` is not defined in terms of bottom. It is a constant in its own right just like `nil` and `cons 1 nil` are. What happ

Note that `false` the value of type `Bool` is not defined in terms of bottom. It is a constant in its own right just like `nil` and `cons 1 nil` are. What happens in Data.Bool is that we have the function from values to types `T` such that `T true` and `T false` are types equal to top and bottom respectively. This value-to-type encoding is called a "universe" and allows us to talk about propositions which are based on boolean function results like theorem1 : T (1 - 1 == 0) which is somewhat interestingly different from theorem2 : 1 - 1 = 0 in that the first will reflect upon the definitions of the (recursive) functions (-) and (==) while the second reflects only upon the definition of (-).