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

Showing changes from revision #0 to #1: Added | ~~Removed~~ | ~~Chan~~ged

Contents

Contents
Definition
See also

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

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