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

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

# Contents

## Definition

A preorder on a type $T$ is a type family $(-)\leq(-)$ over $T$ with

• a family of dependent terms

$a:T, b:T \vdash \pi(a,b):isProp(a \leq b)$

representing that each type $a \leq b$ is a proposition.

• a family of dependent terms

$a:T \vdash \rho(a):a \leq a$

representing the reflexive property of $\leq$.

• a family of dependent terms

$a:T, b:T, c:T \vdash \tau(a, b, c):(a \leq b) \times (b \leq c) \to (a \leq c)$

representing the transitive property of $\leq$.

If $T$ comes with a preorder, then $T$ is a preordered type or a (0,1)-precategory.

## Properties

Every preordered type in a univalent universe is a set and a poset.