#
Homotopy Type Theory
antitonic function > history (Rev #2)

# Contents

## 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

Revision on March 12, 2022 at 18:38:51 by
Anonymous?.
See the history of this page for a list of all contributions to it.