Poset-enriched adjunction (source code)

= Poset-enriched adjunction

In a category whose hom-sets are posets, $f:A\to B$ is left adjoint to $g:B\to A$ when $fg\leq1_B$ and $1_A\leq gf$. Left adjoints are closed under identities and composition.