Homotopy Type Theory monotonic function > history (changes)

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

Contents

< monotonic function

Definition

Let AA and BB be preorders. A monotonic function is a function f:ABf : A \to B with a family of dependent terms

ϕ(a,b):(ab)(f(a)f(b))\phi(a,b):(a \leq b) \to (f(a) \leq f(b))

showing that the preorder is preserved by ff.

See also

Last revised on June 9, 2022 at 19:38:09. See the history of this page for a list of all contributions to it.