Safe Haskell	Safe
Language	Haskell2010

Data.Connection.Property

Description

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, y : x \leq y \Rightarrow f (x) \leq f (y) \)

\( \forall x, y : x \leq y \Rightarrow g (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 \)

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

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

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

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

Synopsis

adjoint :: (Preorder a, Preorder b) => Trip a b -> a -> b -> Bool
adjointL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool
adjointR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool
closed :: (Preorder a, Preorder b) => Trip a b -> a -> Bool
closedL :: (Preorder a, Preorder b) => ConnL a b -> a -> Bool
closedR :: (Preorder a, Preorder b) => ConnR a b -> a -> Bool
kernel :: (Preorder a, Preorder b) => Trip a b -> b -> Bool
kernelL :: (Preorder a, Preorder b) => ConnL a b -> b -> Bool
kernelR :: (Preorder a, Preorder b) => ConnR a b -> b -> Bool
monotonic :: (Preorder a, Preorder b) => Trip a b -> a -> a -> b -> b -> Bool
monotonicR :: (Preorder a, Preorder b) => ConnR a b -> a -> a -> b -> b -> Bool
monotonicL :: (Preorder a, Preorder b) => ConnL a b -> a -> a -> b -> b -> Bool
idempotent :: (Preorder a, Preorder b) => Trip a b -> a -> b -> Bool
idempotentL :: (Preorder a, Preorder b) => ConnL a b -> a -> b -> Bool
idempotentR :: (Preorder a, Preorder b) => ConnR a b -> a -> b -> Bool
monotone :: Rel r Bool -> Rel s Bool -> (r -> s) -> r -> r -> Bool
antitone :: Rel r Bool -> Rel s Bool -> (r -> s) -> r -> r -> Bool
adjunction :: Rel r Bool -> Rel s Bool -> (s -> r) -> (r -> s) -> s -> r -> Bool
range' :: Triple () a => (a, a)
ordering :: Trip () Ordering
invertible :: Rel s b -> (s -> r) -> (r -> s) -> s -> b
projective :: Rel s b -> (r -> s) -> (s -> s) -> r -> b

Documentation

adjoint :: (Preorder a, Preorder b) => Trip a b -> a -> b -> Bool Source #

\( \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.

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

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

closed :: (Preorder a, Preorder b) => Trip a b -> a -> Bool Source #

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

This is a required property.

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

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

kernel :: (Preorder a, Preorder b) => Trip a b -> b -> Bool Source #

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

This is a required property.

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

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

monotonic :: (Preorder a, Preorder b) => Trip a b -> a -> a -> b -> b -> Bool Source #

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

This is a required property.

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

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

idempotent :: (Preorder a, Preorder b) => Trip a b -> a -> b -> Bool Source #

\( \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

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

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

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

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

antitone :: Rel r Bool -> Rel s Bool -> (r -> s) -> r -> r -> Bool Source #

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

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

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

For example, a monotone Galois connection is defined by adjunction (<~) (<~), and an antitone Galois connection is defined by adjunction (>~) (<~).

range' :: Triple () a => (a, a) Source #

ordering :: Trip () Ordering Source #

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

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

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

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

idempotent (#) f = projective (#) f f