connections-0.0.2.2: Partial orders, lattices, & Galois connections.

Safe HaskellSafe
LanguageHaskell2010

Data.Connection.Yoneda

Synopsis

Documentation

type family Rep a :: * Source #

Instances
type Rep Bool Source # 
Instance details

Defined in Data.Connection.Yoneda

type Rep Bool = Bool
type Rep (Down a) Source # 
Instance details

Defined in Data.Connection.Yoneda

type Rep (Down a) = Down (Rep a)

class (Prd a, Lattice (Rep a)) => Yoneda a where Source #

Yoneda representation for lattice ideals & filters.

A subset I of a lattice is an ideal if and only if it is a lower set that is closed under finite joins, i.e., it is nonempty and for all x, y in I, the element x vee y is also in I.

upper and lower commute with Down:

  • lower x y == upper (Down x) (Down y)
  • lower (Down x) (Down y) == upper x y

Rep a is upward-closed:

Rep a is downward-closed:

Finally filter >>> ideal and ideal >>> filter are both connections on a and Rep a respectively.

See:

Methods

ideal :: Conn (Rep a) a Source #

Principal ideal generated by an element of a.

lower :: Rep a -> a -> Bool Source #

Lower set in a generated by an element in Rep a.

filter :: Conn a (Rep a) Source #

Principal filter generated by an element of a.

upper :: Rep a -> a -> Bool Source #

Upper set in a generated by an element in Rep a.

Instances
Yoneda Bool Source # 
Instance details

Defined in Data.Connection.Yoneda

Yoneda a => Yoneda (Down a) Source # 
Instance details

Defined in Data.Connection.Yoneda

Methods

ideal :: Conn (Rep (Down a)) (Down a) Source #

lower :: Rep (Down a) -> Down a -> Bool Source #

filter :: Conn (Down a) (Rep (Down a)) Source #

upper :: Rep (Down a) -> Down a -> Bool Source #