# Homotopy Type Theory setoid > history (Rev #1)

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