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

Showing changes from revision #2 to #3: 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 June 9, 2022 at 23:38:09 by Anonymous?. See the history of this page for a list of all contributions to it.