Homotopy Type Theory antitonic function > history (changes)

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

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$.