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

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$

category: not redirected to nlab yet

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