Homotopy Type Theory set > history (changes)

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

Contents

Definition

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

Last revised on June 17, 2022 at 18:07:49. See the history of this page for a list of all contributions to it.