Data.Connection.Property

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

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

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

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

Adjointness

adjoint :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> b -> Bool

adjointL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool

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

A Galois connection is an adjunction of preorders. This is a required property.

adjointR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool

adjunction :: Rel r Bool -> Rel s Bool -> (s -> r) -> (r -> s) -> s -> r -> Bool

\( \forall a: f a \leq b \Leftrightarrow a \leq g b \)

A monotone Galois connection is defined by adjunction (<~) (<~), while an antitone Galois connection is defined by adjunction (>~) (<~).

Closure

closed :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> Bool

closedL :: (Preorder a, Preorder b) => ConnL a b -> a -> Bool

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

This is a required property.

closedR :: (Preorder a, Preorder b) => ConnR a b -> a -> Bool

kernel :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> b -> Bool

kernelL :: (Preorder a, Preorder b) => ConnL a b -> b -> Bool

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

This is a required property.

kernelR :: (Preorder a, Preorder b) => ConnR a b -> b -> Bool

invertible :: Rel s b -> (s -> r) -> (r -> s) -> s -> b

\( \forall a: f (g a) \sim a \)

Monotonicity

monotonic :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> a -> b -> b -> Bool

monotonicR :: (Preorder a, Preorder b) => ConnR a b -> a -> a -> b -> b -> Bool

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

This is a required property.

monotonicL :: (Preorder a, Preorder b) => ConnL a b -> a -> a -> b -> b -> Bool

monotone :: Rel r Bool -> Rel s Bool -> (r -> s) -> r -> r -> Bool

\( \forall a, b: a \leq b \Rightarrow f(a) \leq f(b) \)

Idempotence

idempotent :: (Preorder a, Preorder b) => (forall k. Conn k a b) -> a -> b -> Bool

idempotentL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool

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

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

idempotentR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool

projective :: Rel s b -> (r -> s) -> (s -> s) -> r -> b

\( \forall a: g \circ f (a) \sim f (a) \)