[[!redirects setoids]] [[!redirects equivalence relation]] [[!redirects equivalence relations]] ## Contents ## * table of contents {:toc} ## 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**. ## See also ## * [[pregroupoid]] * [[directed graph]] * [[quotient set]] * [[univalent setoid]] * [[decidable setoid]]