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