Data.Connection.Yoneda

Documentation

type family Rep a :: *

Instances

type Rep Bool

Defined in Data.Connection.Yoneda

type Rep Bool = Bool

type Rep (Down a)

Defined in Data.Connection.Yoneda

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

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

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:

• upper x s && x y == upper y s

• upper x s && upper y s ==> connl filter x / connl filter y >~ s

Rep a is downward-closed:

• lower x s && x >~ y ==> lower y s

• lower x s && lower y s ==> connl ideal x / connl ideal y ~< s

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

See also:

• https://en.wikipedia.org/wiki/Filter_(mathematics)
• https://en.wikipedia.org/wiki/Ideal_(order_theory)

Methods

ideal :: Conn (Rep a) a

lower :: Rep a -> a -> Bool

filter :: Conn a (Rep a)

upper :: Rep a -> a -> Bool

Instances

Yoneda Bool

Defined in Data.Connection.Yoneda

Methods

ideal :: Conn (Rep Bool) Bool

lower :: Rep Bool -> Bool -> Bool

filter :: Conn Bool (Rep Bool)

upper :: Rep Bool -> Bool -> Bool