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 | ||
|
set_._hott [2014/11/11 22:16] nikolaj |
set_._hott [2014/11/17 19:16] nikolaj |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| ==== 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 === | ||
| Line 12: | Line 12: | ||
| ==== Parents ==== | ==== Parents ==== | ||
| === Requirements === | === Requirements === | ||
| - | [[Identity type]] | + | [[Mere proposition]] |
