Algebra.Heyting

Documentation

class BoundedLattice a => Heyting a where

A Heyting algebra is a bounded lattice equipped with a binary operation \(a \to b\) of implication.

Laws

x ==> x        ≡ top
x /\ (x ==> y) ≡ x /\ y
y /\ (x ==> y) ≡ y
x ==> (y /\ z) ≡ (x ==> y) /\ (x ==> z)

Minimal complete definition

(==>)

Methods

(==>) :: a -> a -> a infixr 5

Implication.

neg :: a -> a

Negation.

neg x = x ==> bottom

(<=>) :: a -> a -> a infixr 5

Equivalence.

x <=> y = (x ==> y) /\ (y ==> x)

Instances

Heyting Bool

Defined in Algebra.Heyting

Methods

(==>) :: Bool -> Bool -> Bool

neg :: Bool -> Bool

(<=>) :: Bool -> Bool -> Bool

Heyting ()

Defined in Algebra.Heyting

Methods

(==>) :: () -> () -> ()

neg :: () -> ()

(<=>) :: () -> () -> ()

Heyting All

Defined in Algebra.Heyting

Methods

(==>) :: All -> All -> All

neg :: All -> All

(<=>) :: All -> All -> All

Heyting Any

Defined in Algebra.Heyting

Methods

(==>) :: Any -> Any -> Any

neg :: Any -> Any

(<=>) :: Any -> Any -> Any

Heyting ZeroHalfOne

Not boolean: neg Half \/ Half = Half /= One

Defined in Algebra.Lattice.ZeroHalfOne

Methods

(==>) :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne

neg :: ZeroHalfOne -> ZeroHalfOne

(<=>) :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne

Heyting M2

Defined in Algebra.Lattice.M2

Methods

(==>) :: M2 -> M2 -> M2

neg :: M2 -> M2

(<=>) :: M2 -> M2 -> M2

Heyting a => Heyting (Identity a)

Defined in Algebra.Heyting

Methods

(==>) :: Identity a -> Identity a -> Identity a

neg :: Identity a -> Identity a

(<=>) :: Identity a -> Identity a -> Identity a

Heyting a => Heyting (Endo a)

Defined in Algebra.Heyting

Methods

(==>) :: Endo a -> Endo a -> Endo a

neg :: Endo a -> Endo a

(<=>) :: Endo a -> Endo a -> Endo a

(Ord a, Finite a) => Heyting (Set a)

Defined in Algebra.Heyting

Methods

(==>) :: Set a -> Set a -> Set a

neg :: Set a -> Set a

(<=>) :: Set a -> Set a -> Set a

(Eq a, Hashable a, Finite a) => Heyting (HashSet a)

Defined in Algebra.Heyting

Methods

(==>) :: HashSet a -> HashSet a -> HashSet a

neg :: HashSet a -> HashSet a

(<=>) :: HashSet a -> HashSet a -> HashSet a

(Ord a, Bounded a) => Heyting (Ordered a)

This is interesting logic, as it satisfies both de Morgan laws; but isn't Boolean: i.e. law of exluded middle doesn't hold.

Negation "smashes" value into minBound or maxBound.

Defined in Algebra.Lattice.Ordered

Methods

(==>) :: Ordered a -> Ordered a -> Ordered a

neg :: Ordered a -> Ordered a

(<=>) :: Ordered a -> Ordered a -> Ordered a

Heyting (Free a)

Defined in Algebra.Heyting.Free

Methods

(==>) :: Free a -> Free a -> Free a

neg :: Free a -> Free a

(<=>) :: Free a -> Free a -> Free a

Heyting a => Heyting (b -> a)

Defined in Algebra.Heyting

Methods

(==>) :: (b -> a) -> (b -> a) -> b -> a

neg :: (b -> a) -> b -> a

(<=>) :: (b -> a) -> (b -> a) -> b -> a

Heyting (Proxy a)

Defined in Algebra.Heyting

Methods

(==>) :: Proxy a -> Proxy a -> Proxy a

neg :: Proxy a -> Proxy a

(<=>) :: Proxy a -> Proxy a -> Proxy a

Heyting a => Heyting (Const a b)

Defined in Algebra.Heyting

Methods

(==>) :: Const a b -> Const a b -> Const a b

neg :: Const a b -> Const a b

(<=>) :: Const a b -> Const a b -> Const a b

Heyting a => Heyting (Tagged b a)

Defined in Algebra.Heyting

Methods

(==>) :: Tagged b a -> Tagged b a -> Tagged b a

neg :: Tagged b a -> Tagged b a

(<=>) :: Tagged b a -> Tagged b a -> Tagged b a