Showing changes from revision #8 to #9:
Added | ~~Removed~~ | ~~Chan~~ged

A **set** consists of

- A type $A$
- A
~~0-truncator~~set-truncator$${\tau}_{0}:\prod _{(a:A)}\prod _{(b:A)}\mathrm{isProp}\prod _{c:(a=b)}(\prod _{d:(a=b)}\mathrm{ac}=\mathrm{bd})$$ \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

category: not redirected to nlab yet