connections-0.0.2.1: Partial orders & 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:

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

Methods

ideal :: Conn (Rep a) a Source #

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

filter :: Conn a (Rep a) Source #

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

Instances
Yoneda Bool Source # 
Instance details

Defined in Data.Connection.Yoneda