Documentation

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

A monotone Galois connection.

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

This is a required property.

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

This is a required property.

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

This is a required property.

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

This is a required property.

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

This is a required property.

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

This is a required property.

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

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

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

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

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

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