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

Contents

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

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