Homotopy Type Theory set > history (Rev #9)



A set consists of

  • A type AA
  • A set-truncator
    τ 0: a:A b:A c:(a=b) d:(a=b)c=d\tau_0: \prod_{a:A} \prod_{b:A} \prod_{c:(a = b)} \prod_{d:(a = b)} c = d

See also

Revision on June 16, 2022 at 12:03:32 by Anonymous?. See the history of this page for a list of all contributions to it.