Safe Haskell	None
Language	Haskell2010

Algebra.Boolean

Contents

Adjunction between Boolean and Heyting algebras

Synopsis

data BooleanAlgebra a
(==>) :: Heyting a => a -> a -> a
neg :: Heyting a => a -> a
class Heyting a => Boolean a
runBooleanAlgebra :: BooleanAlgebra a -> a
boolean :: Heyting a => a -> BooleanAlgebra a

Documentation

data BooleanAlgebra a Source #

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

Instances

Instances details

Bounded a => Bounded (BooleanAlgebra a) Source #
Instance details Defined in Algebra.Boolean Methods minBound :: BooleanAlgebra a # maxBound :: BooleanAlgebra a #
Eq a => Eq (BooleanAlgebra a) Source #
Instance details Defined in Algebra.Boolean Methods (==) :: BooleanAlgebra a -> BooleanAlgebra a -> Bool # (/=) :: BooleanAlgebra a -> BooleanAlgebra a -> Bool #
Data a => Data (BooleanAlgebra a) Source #
Instance details Defined in Algebra.Boolean Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BooleanAlgebra a -> c (BooleanAlgebra a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (BooleanAlgebra a) # toConstr :: BooleanAlgebra a -> Constr # dataTypeOf :: BooleanAlgebra a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (BooleanAlgebra a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (BooleanAlgebra a)) # gmapT :: (forall b. Data b => b -> b) -> BooleanAlgebra a -> BooleanAlgebra a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BooleanAlgebra a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BooleanAlgebra a -> r # gmapQ :: (forall d. Data d => d -> u) -> BooleanAlgebra a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BooleanAlgebra a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BooleanAlgebra a -> m (BooleanAlgebra a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BooleanAlgebra a -> m (BooleanAlgebra a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BooleanAlgebra a -> m (BooleanAlgebra a) #
Ord a => Ord (BooleanAlgebra a) Source #
Instance details Defined in Algebra.Boolean Methods compare :: BooleanAlgebra a -> BooleanAlgebra a -> Ordering # (<) :: BooleanAlgebra a -> BooleanAlgebra a -> Bool # (<=) :: BooleanAlgebra a -> BooleanAlgebra a -> Bool # (>) :: BooleanAlgebra a -> BooleanAlgebra a -> Bool # (>=) :: BooleanAlgebra a -> BooleanAlgebra a -> Bool # max :: BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a # min :: BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a #
Read a => Read (BooleanAlgebra a) Source #
Instance details Defined in Algebra.Boolean Methods readsPrec :: Int -> ReadS (BooleanAlgebra a) # readList :: ReadS [BooleanAlgebra a] # readPrec :: ReadPrec (BooleanAlgebra a) # readListPrec :: ReadPrec [BooleanAlgebra a] #
Show a => Show (BooleanAlgebra a) Source #
Instance details Defined in Algebra.Boolean Methods showsPrec :: Int -> BooleanAlgebra a -> ShowS # show :: BooleanAlgebra a -> String # showList :: [BooleanAlgebra a] -> ShowS #
Generic (BooleanAlgebra a) Source #
Instance details Defined in Algebra.Boolean Associated Types type Rep (BooleanAlgebra a) :: Type -> Type # Methods from :: BooleanAlgebra a -> Rep (BooleanAlgebra a) x # to :: Rep (BooleanAlgebra a) x -> BooleanAlgebra a #
Heyting a => Heyting (BooleanAlgebra a) Source #
Instance details Defined in Algebra.Boolean Methods (==>) :: BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a # neg :: BooleanAlgebra a -> BooleanAlgebra a # (<=>) :: BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a #
Lattice a => Lattice (BooleanAlgebra a) Source #
Instance details Defined in Algebra.Boolean Methods (\/) :: BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a # (/\) :: BooleanAlgebra a -> BooleanAlgebra a -> BooleanAlgebra a #
BoundedJoinSemiLattice a => BoundedJoinSemiLattice (BooleanAlgebra a) Source #
Instance details Defined in Algebra.Boolean Methods bottom :: BooleanAlgebra a #
BoundedMeetSemiLattice a => BoundedMeetSemiLattice (BooleanAlgebra a) Source #
Instance details Defined in Algebra.Boolean Methods top :: BooleanAlgebra a #
Heyting a => Boolean (BooleanAlgebra a) Source #
Instance details Defined in Algebra.Boolean
type Rep (BooleanAlgebra a) Source #
Instance details Defined in Algebra.Boolean type Rep (BooleanAlgebra a) = D1 ('MetaData "BooleanAlgebra" "Algebra.Boolean" "heyting-algebras-0.2.0.1-ESmFQmKgxne8K6ZOTNu8qI" 'True) (C1 ('MetaCons "BooleanAlgebra" 'PrefixI 'True) (S1 ('MetaSel ('Just "runBooleanAlgebra") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

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

Implication.

neg :: Heyting a => a -> a #

Negation.

neg x = x ==> bottom

Adjunction between Boolean and Heyting algebras

class Heyting a => Boolean a Source #

Instances

Instances details

Boolean Bool Source #
Instance details Defined in Algebra.Boolean
Boolean () Source #
Instance details Defined in Algebra.Boolean
Boolean All Source #
Instance details Defined in Algebra.Boolean
Boolean Any Source #
Instance details Defined in Algebra.Boolean
Boolean a => Boolean (Identity a) Source #
Instance details Defined in Algebra.Boolean
Boolean a => Boolean (Endo a) Source #
Instance details Defined in Algebra.Boolean
Heyting a => Boolean (BooleanAlgebra a) Source #
Instance details Defined in Algebra.Boolean
Boolean (FreeBoolean a) Source #
Instance details Defined in Algebra.Boolean.Free
Boolean b => Boolean (a -> b) Source #
Instance details Defined in Algebra.Boolean
Boolean (Proxy a) Source #
Instance details Defined in Algebra.Boolean
Boolean a => Boolean (Const a b) Source #
Instance details Defined in Algebra.Boolean
Boolean a => Boolean (Tagged t a) Source #
Instance details Defined in Algebra.Boolean

runBooleanAlgebra :: BooleanAlgebra a -> a Source #

extract value from Boolean

boolean :: Heyting a => a -> BooleanAlgebra a Source #

Smart constructro of the Boolean type.