Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
set_._hott [2014/11/11 22:16] nikolaj |
set_._hott [2016/01/16 18:27] nikolaj |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ===== Set . HoTT ===== | ===== Set . HoTT ===== | ||
| ==== Type ==== | ==== Type ==== | ||
| - | $isSet(A):={\large\Pi}_{x,y:A}\,isProp(Id_A(x,y))$ | + | ${\mathrm{isSet}}(A):={\large\Pi}_{x,y:A}\,isProp(Id_A(x,y))$ |
| ==== Discussion ==== | ==== Discussion ==== | ||
| === Elaboration === | === Elaboration === | ||
| - | The sets as defined in HoTT are easier to understand when contrasted against more difficult structures. For example, //if we consider two groups// $G,G':groups$ which are isomorphic in five different ways (isomorphism will be defined as invertible group homomorphism in this case), then, due to the existence on //an// isomorphism they are the same for all practical purposes. All five isomorphisms demonstrate $G=_{group}G'$. Thinking in terms of set theoretic models of a group, an isomorphism might permute elements $x,y$ of $G$ while keeping $G$s group structure intact. Now //if we consider two elements of a set// $x,y:A$, then since being together in a set shouldn't constitute any structural relations, there are also no elaborate means of them being the same, unless the expressions $x$ and $y$ can be tracked back to come from the same definition, i.e. if they are definitionally the same. The definition above says that a type $A$ is a set if the identity on their elements doesn't derive from interesting isomorphisms but is just am matter of yes or no. | + | See the last lines of [[univalence axiom]]. |
| === Alternative definitions === | === Alternative definitions === | ||
| - | $isSet(A):={\large\Pi}_{x,y:A}{\large\Pi}_{p,q:Id_A(x,y)}\,Id_{Id_A(x,y)}(p,q)$ | + | ${\mathrm{isSet}}(A):={\large\Pi}_{x,y:A}\,{\large\Pi}_{p,q: {\mathrm {Id}}_A(x,y)}\,{\mathrm {Id}}_{{\mathrm {Id}}_A(x,y)}(p,q)$ |
| + | |||
| + | ${\mathrm{isSet}}(A):={\large\Pi}(x,y:A)\,{\large\Pi}(p,q: {\mathrm {Id}}_A(x,y))\,{\mathrm {Id}}_{{\mathrm {Id}}_A(x,y)}(p,q)$ | ||
| === Reference === | === Reference === | ||
| ==== Parents ==== | ==== Parents ==== | ||
| === Requirements === | === Requirements === | ||
| - | [[Identity type]] | + | [[Mere proposition]] |
