# Homotopy Type Theory monotonic function > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

# Contents

## Definition

Let $A$ and $B$ be preorders. 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$.