# Homotopy Type Theory setoid > history (changes)

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

## Definition

A setoid is a preordered type $(T, \equiv)$ with a term

$s: \prod_{a:A} \prod_{b:A} (a \equiv b) \to (b \equiv a)$

The preorder $\equiv$ is called an equivalence relation.