Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
subset_._hott [2014/11/11 17:50] nikolaj |
subset_._hott [2014/11/11 17:55] nikolaj |
||
|---|---|---|---|
| Line 11: | Line 11: | ||
| * $\{x\,|\,Q(x)\}\subseteq\{x\,|\,P(x)\}\equiv {\large\Pi}_{x:A}\left(Q(x)\to P(x)\right)$ | * $\{x\,|\,Q(x)\}\subseteq\{x\,|\,P(x)\}\equiv {\large\Pi}_{x:A}\left(Q(x)\to P(x)\right)$ | ||
| - | 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 contain 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)\equiv A\to\Omega$, where $\Omega$ is some appropriate truth value object. |
| - | "${\large\frac{x\,:\,A\,\vdash\,P(x)\,:\,\mathrm{Prop}}{\{x\,|\,P(x)\}\,:\,\mathcal{P}(A)}}$". | + | |
| ==== Discussion ==== | ==== Discussion ==== | ||
