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

Showing changes from revision #5 to #6: Added | Removed | Changed

Contents

Definition

A set consists of

• A type $A$
• A 0-truncator
  $${\tau }_0:\prod _{(a:A)}\prod _{(b:A)}\prod _{(c:a=b)}\mathrm{isProp}\prod _{(d:a=b)}(\sum _{(x:c=d)}a\prod _{(y:c=d)}x=\mathrm{<span><del\; class="diffmod">\; y</del><ins\; class="diffmod">\; b</ins></span>})$$ \tau_0: \prod_{(a:A)} \prod_{(b:A)} \prod_{(c:a=b)} \mathrm{isProp}(a \prod_{(d:a=b)} = \sum_{(x:c=d)} b) \prod_{(y:c=d)} x=y

As univalent setoids

A set is a setoid $T$ where the canonical functions

are equivalences

Examples

• A monoid is a set that is also an A3-space.

See also

• contractible type

• proposition

• groupoid

• homotopy level

• setoid

References

• HoTT book