Homotopy Type Theory monotonic function > history (Rev #1)

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?

Revision on March 11, 2022 at 01:13:08 by Anonymous?. See the history of this page for a list of all contributions to it.