#
Homotopy Type Theory
antitonic function > history (changes)

Showing changes from revision #2 to #3:
Added | ~~Removed~~ | ~~Chan~~ged

# Contents

< antitonic function

~~
~~## Definition

~~
~~Let $A$ and $B$ be preorders. An **antitonic function** is a function $f : A \to B$ with a family of dependent terms

~~
~~$\phi(a,b):(a \leq b) \to (f(b) \leq f(a))$

~~
~~showing that the preorder is reversed by $f$.

~~
~~## See also

~~
~~
Last revised on June 9, 2022 at 23:36:29.
See the history of this page for a list of all contributions to it.