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

## Contents

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

Revision on April 27, 2022 at 11:37:30 by
Anonymous?.
See the history of this page for a list of all contributions to it.