Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
subset_._hott [2014/11/11 17:49] nikolaj |
subset_._hott [2014/11/11 17:55] (current) 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{A\,:\,\mathrm{Set}\hspace{.5cm}x\,:\,A\,\vdash\,P(x)\,:\,\mathrm{Prop}}{\{x\,|\,P(x)\}\,:\,\mathcal{P}(A)}}$". | + | |
==== Discussion ==== | ==== Discussion ==== |