connections-0.0.2.1: Partial orders & Galois connections.

Data.Connection.Yoneda

Synopsis

# Documentation

type family Rep a :: * Source #

Instances
 type Rep Bool Source # Instance detailsDefined in Data.Connection.Yoneda type Rep Bool = Bool type Rep (Down a) Source # Instance detailsDefined 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:

• 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.