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

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

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 12, 2022 at 18:07:29 by Anonymous?. See the history of this page for a list of all contributions to it.