# Homotopy Type Theory set > history (Rev #6)

## Definition

A set consists of

• A type $A$
• A 0-truncator
$\tau_0: \prod_{(a:A)} \prod_{(b:A)} \mathrm{isProp}(a = b)$

### As univalent setoids

A set is a setoid $T$ where the canonical functions

$a:T, b:T \vdash idtoiso(a,b):(a =_T b) \to (a \equiv b)$

are equivalences

$p: \prod_{a:A} \prod_{b:A} (a =_T b) \cong (a \equiv b)$

## References

Revision on May 1, 2022 at 21:40:01 by Anonymous?. See the history of this page for a list of all contributions to it.