Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
subset_._hott [2014/11/11 17:50]
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 $\Omegais some appropriate truth value object.
-"${\large\frac{x\,:​\,​A\,\vdash\,P(x)\,:​\,​\mathrm{Prop}}{\{x\,​|\,​P(x)\}\,:​\,​\mathcal{P}(A)}}$".+
  
 ==== Discussion ==== ==== Discussion ====
Link to graph
Log In
Improvements of the human condition