Differences
This shows you the differences between two versions of the page.
Both sides previous 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 | ||
- | "${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 ==== |