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

Showing changes from revision #8 to #9: Added | Removed | Changed



A set consists of

  • A type AA
  • A 0-truncator set-truncator
    τ 0: (a:A) (b:A)isProp c:(a=b)( d:(a=b) a c= b d) \tau_0: \prod_{(a:A)} \prod_{a:A} \prod_{(b:A)} \prod_{b:A} \mathrm{isProp}(a \prod_{c:(a = b) 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.