Homotopy Type Theory set > history (Rev #3)

Definition

A set consists of

  • A type AA
  • A 0-truncator
    τ 0: (a:A) (b:A) (c:a=b) (d:a=b) (x:c=d) (y:c=d)x=y\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

Examples

See also

References

Revision on February 13, 2022 at 19:58:42 by Anonymous?. See the history of this page for a list of all contributions to it.