#Contents# * table of contents {:toc} ## Definition ## Let $A$ and $B$ be [[preorder]]s. A __monotonic function__ is a function $f : A \to B$ with a family of dependent terms $$\phi(a,b):(a \leq b) \to (f(a) \leq f(b))$$ showing that the preorder is preserved by $f$. ## See also ## * [[functor]] * [[monotonic function preorder]]