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

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

Contents

Definition
See also

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$ .

See also

functor
monotonic function preorder?

antitonic function

Revision on March 12, 2022 at 23:07:29 by Anonymous?. See the history of this page for a list of all contributions to it.