Homotopy Type Theory set > history (Rev #9)

Contents

Definition

A set consists of

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

See also

• proposition