Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
subset_._hott [2014/11/11 17:48] nikolaj |
subset_._hott [2014/11/11 17:49] nikolaj |
||
|---|---|---|---|
| Line 13: | Line 13: | ||
| The first identification corresponds to the axiom schema of replacement (or similar axioms like collection and specification). The second notion is different from most set theories written down in a predicate logic in that the subset doesn't contain $a$ itself but a tagged version $\langle a,\star_a\rangle$ of it. With regard to the third notion it must be emphasizes that here sets don't contain sets that conain sets, etc., as e.g. in ZFC. | The first identification corresponds to the axiom schema of replacement (or similar axioms like collection and specification). The second notion is different from most set theories written down in a predicate logic in that the subset doesn't contain $a$ itself but a tagged version $\langle a,\star_a\rangle$ of it. With regard to the third notion it must be emphasizes that here sets don't contain sets that conain sets, etc., as e.g. in ZFC. | ||
| - | One can go further and work out a notion of power set "$\mathcal{P}(A)$" with type constructor along the lines of | + | One can go further and work out a notion of power set $\mathcal{P}(A)$ with type constructor along the lines of |
| - | "${\large\frac{A\,:\,\mathrm{Set}\hspace{.5cm}x\,:\,A\,\vdash\,P(x)\,:\,\mathrm{Prop}}{\{x\,|\,P(x)\}\,:\,\mathcal{P}(A)}}$". | + | "${x\,:\,A\,\vdash\,P(x)\,:\,\mathrm{Prop}}{\{x\,|\,P(x)\}\,:\,\mathcal{P}(A)}}$". |
| ==== Discussion ==== | ==== Discussion ==== | ||
