# Homotopy Type Theory set > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

## Definition

A set is consists a of 0-truncated? type.

• A type $A$
• A 0-truncator
$\tau_0: \prod_{(a:A)} \prod_{(b:A)} \prod_{(c:a=b)} \prod_{(d:a=b)} \sum_{(x:c=d)} \prod_{(y:c=d)} x=y$

## References

Revision on February 3, 2022 at 23:41:51 by Anonymous?. See the history of this page for a list of all contributions to it.