Data.Connection

Connection

data Conn a b

A Galois connection between two monotone functions: \(connl \dashv connr \)

Each side of the adjunction may be defined in terms of the other:

\( connr(x) = \sup \{y \in E \mid connl(y) \leq x \} \)

\( connl(x) = \inf \{y \in E \mid connr(y) \geq x \} \)

Galois connections have the same properties as adjunctions defined over other categories:

\( \forall x, y : connl \dashv connr \Rightarrow connl (x) \leq b \Leftrightarrow x \leq connr (y) \)

\( \forall x, y : x \leq y \Rightarrow connl (x) \leq connl (y) \)

\( \forall x, y : x \leq y \Rightarrow connr (x) \leq connr (y) \)

\( \forall x : connl \dashv connr \Rightarrow x \leq connr \circ connl (x) \)

\( \forall x : connl \dashv connr \Rightarrow connl \circ connr (x) \leq x \)

\( \forall x : unit \circ unit (x) \sim unit (x) \)

\( \forall x : counit \circ counit (x) \sim counit (x) \)

\( \forall x : counit \circ connl (x) \sim connl (x) \)

\( \forall x : unit \circ connr (x) \sim connr (x) \)

See also Property and https://en.wikipedia.org/wiki/Galois_connection.

Constructors

Conn (a -> b) (b -> a)

Instances

Category Conn

Defined in Data.Connection

Methods

id :: Conn a a

(.) :: Conn b c -> Conn a b -> Conn a c

connl :: Prd a => Prd b => Conn a b -> a -> b

connr :: Prd a => Prd b => Conn a b -> b -> a

unit :: Prd a => Prd b => Conn a b -> a -> a

counit :: Prd a => Prd b => Conn a b -> b -> b

pcomparing :: Eq b => Prd a => Prd b => Conn a b -> a -> a -> Maybe Ordering

Partial version of comparing.

Helpful in conjunction with the xxxBy functions from List.

dual :: Prd a => Prd b => Conn a b -> Conn (Down b) (Down a)

(***) :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (a, c) (b, d) infixr 3

(+++) :: Prd a => Prd b => Prd c => Prd d => Conn a b -> Conn c d -> Conn (Either a c) (Either b d) infixr 2

(&&&) :: Prd a => Prd b => Lattice c => Conn c a -> Conn c b -> Conn c (a, b) infixr 3

(|||) :: Prd a => Prd b => Prd c => Conn a c -> Conn b c -> Conn (Either a b) c infixr 2

_1 :: Prd a => Prd b => Prd c => Conn a b -> Conn (a, c) (b, c)

Lens into first part of a product.

_1 (ab >>> cd) = _1 ab >>> _1 cd

_2 :: Prd a => Prd b => Prd c => Conn a b -> Conn (c, a) (c, b)

_L :: Prd a => Prd b => Prd c => Conn a b -> Conn (Either a c) (Either b c)

Prism into left part of a sum.

_L (ab >>> cd) = _L ab >>> _L cd

_R :: Prd a => Prd b => Prd c => Conn a b -> Conn (Either c a) (Either c b)

just :: Prd a => Prd b => Conn a b -> Conn (Maybe a) (Maybe b)

list :: Prd a => Prd b => Conn a b -> Conn [a] [b]

binord :: Conn Bool Ordering

ordbin :: Conn Ordering Bool

Triple

data Trip a b

An adjoint triple.

Trip f g h satisfies:

f ⊣ g ⊥ ⊥ g ⊣ h

See https://ncatlab.org/nlab/show/adjoint+triple

Constructors

Trip (a -> b) (b -> a) (a -> b)

Instances

Category Trip

Defined in Data.Connection

Methods

id :: Trip a a

(.) :: Trip b c -> Trip a b -> Trip a c

tripl :: Prd a => Prd b => Trip a b -> Conn a b

tripr :: Prd a => Prd b => Trip a b -> Conn b a

unitl :: Prd a => Prd b => Trip a b -> a -> a

unitr :: Prd a => Prd b => Trip a b -> b -> b

counitl :: Prd a => Prd b => Trip a b -> b -> b

counitr :: Prd a => Prd b => Trip a b -> a -> a

ceiling' :: Prd a => Prd b => Trip a b -> a -> b

floor' :: Prd a => Prd b => Trip a b -> a -> b

(****) :: Prd a => Prd b => Prd c => Prd d => Trip a b -> Trip c d -> Trip (a, c) (b, d) infixr 3

(++++) :: Prd a => Prd b => Prd c => Prd d => Trip a b -> Trip c d -> Trip (Either a c) (Either b d) infixr 2

(&&&&) :: Prd a => Prd b => Lattice c => Trip a c -> Trip b c -> Trip (a, b) c infixr 3

(||||) :: Prd a => Prd b => Prd c => Trip c a -> Trip c b -> Trip c (Either a b) infixr 2

_1' :: Prd a => Prd b => Prd c => Trip a b -> Trip (a, c) (b, c)

_2' :: Prd a => Prd b => Prd c => Trip a b -> Trip (c, a) (c, b)

_L' :: Prd a => Prd b => Prd c => Trip a b -> Trip (Either a c) (Either b c)

_R' :: Prd a => Prd b => Prd c => Trip a b -> Trip (Either c a) (Either c b)

diag :: Lattice a => Trip (a, a) a

codiag :: Prd a => Trip a (Either a a)

bound :: Prd a => Bound a => Trip () a

maybel :: Prd a => Bound b => Trip (Maybe a) (Either a b)

mayber :: Prd b => Bound a => Trip (Maybe b) (Either a b)