Safe Haskell | None |
---|---|

Language | Haskell2010 |

## Synopsis

- class HeytingAlgebra a => BooleanAlgebra a
- (==>) :: HeytingAlgebra a => a -> a -> a
- not :: HeytingAlgebra a => a -> a
- iff :: HeytingAlgebra a => a -> a -> a
- iff' :: (Eq a, HeytingAlgebra a) => a -> a -> Bool
- data Boolean a
- runBoolean :: Boolean a -> a
- boolean :: HeytingAlgebra a => a -> Boolean a

# Documentation

class HeytingAlgebra a => BooleanAlgebra a Source #

Boolean algebra is a Heyting algebra which negation satisfies the law of excluded middle, i.e. either of the following:

not . not == not

or

x ∨ not x == top

Another characterisation of Boolean algebras is as complemented distributive lattices where the complement satisfies the following three properties:

(not a) ∧ a == bottom and (not a) ∨ a == top -- excluded middle law

not (not a) == a -- involution law

a ≤ b ⇒ not b ≤ not a -- order-reversing

## Instances

(==>) :: HeytingAlgebra a => a -> a -> a infixr 4 Source #

not :: HeytingAlgebra a => a -> a Source #

# Adjunction between Boolean and Heyting algebras

is the left adjoint functor from the category of Heyting algebras
to the category of Boolean algebras; its right adjoint is the inclusion.`Boolean`

## Instances

runBoolean :: Boolean a -> a Source #

extract value from `Boolean`