Loading [MathJax]/jax/output/HTML-CSS/jax.js

connections-0.3.1: Orders, Galois connections, and lattices.

Safe HaskellSafe
LanguageHaskell2010

Data.Connection.Property

Contents

Description

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

x,y:fgf(x)bxg(y)

x:fgxgf(x)

x:fgfg(x)x

Synopsis

Adjointness

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

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

x,y:fgf(x)yxg(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 Source #

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

a:fabagb

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 Source #

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

x:fgxgf(x)

This is a required property.

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

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

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

x:fgxgf(x)

This is a required property.

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

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

a:f(ga)a

Monotonicity

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

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

x,y:xyf(x)f(y)

This is a required property.

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

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

a,b:abf(a)f(b)

Idempotence

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

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

x:fgcounitf(x)f(x)unitg(x)g(x)

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

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

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

a:gf(a)f(a)