# Homotopy Type Theory opposite preorder > history (Rev #2, changes)

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

# Contents

## Definition

Given a preorder or (0,1)-precategory $P \coloneqq (F(P), \leq)$, an opposite preorder or opposite (0,1)-precategory is a preorder $P^\op \coloneqq (F(P), \geq)$ with $\geq$ defined as

$a:F(P), b:F(P) \vdash a \geq b \coloneqq b \leq a$

where $F$ is the forgetful functor that gets the underlying type for a preorder.