Data.Connection.Property

Documentation

connection :: Prd a => Prd b => Conn a b -> a -> b -> Bool

\( \forall x, y : f \dashv g \Rightarrow f (x) \leq y \Leftrightarrow x \leq g (y) \)

A monotone Galois connection.

closed :: Prd a => Prd b => Conn a b -> a -> Bool

\( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \)

This is a required property.

closed' :: Prd a => Prd b => Trip a b -> a -> Bool

\( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \)

This is a required property.

kernel :: Prd a => Prd b => Conn a b -> b -> Bool

\( \forall x : f \dashv g \Rightarrow f \circ g (x) \leq x \)

This is a required property.

kernel' :: Prd a => Prd b => Trip a b -> b -> Bool

\( \forall x : f \dashv g \Rightarrow x \leq g \circ f (x) \)

This is a required property.

monotone :: Prd a => Prd b => Conn a b -> b -> b -> Bool

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

This is a required property.

monotone' :: Prd a => Prd b => Conn a b -> a -> a -> Bool

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

This is a required property.

idempotent_unit :: Prd a => Prd b => Conn a b -> a -> Bool

\( \forall x : f \dashv g \Rightarrow unit \circ unit (x) \sim unit (x) \)

idempotent_counit :: Prd a => Prd b => Conn a b -> b -> Bool

\( \forall x : f \dashv g \Rightarrow counit \circ counit (x) \sim counit (x) \)

projective_l :: Prd a => Prd b => Conn a b -> a -> Bool

\( \forall x: f \dashv g \Rightarrow counit \circ f (x) \sim f (x) \)

See https://ncatlab.org/nlab/show/idempotent+adjunction

projective_r :: Prd a => Prd b => Conn a b -> b -> Bool

\( \forall x: f \dashv g \Rightarrow unit \circ g (x) \sim g (x) \)

See https://ncatlab.org/nlab/show/idempotent+adjunction