Showing changes from revision #5 to #6:
Added | ~~Removed~~ | ~~Chan~~ged

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{yb})$$ \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~~

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

$a:T, b:T \vdash idtoiso(a,b):(a =_T b) \to (a \equiv b)$

are equivalences

$p: \prod_{a:A} \prod_{b:A} (a =_T b) \cong (a \equiv b)$