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