Homotopy Type Theory setoid > history (changes)

Showing changes from revision #1 to #2: 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

Last revised on June 15, 2022 at 20:39:35. See the history of this page for a list of all contributions to it.