Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
univalence_axiom [2014/11/18 13:30] nikolaj |
univalence_axiom [2016/07/18 01:02] nikolaj |
||
|---|---|---|---|
| Line 25: | Line 25: | ||
| In set theory, we can make //models// of other structures so that truths of their theories are reflected as truths of sets. For example, one commonly defines ${\bar 0}\equiv\{\}$, ${\bar S}x\equiv x\cup\{x\}$ and addition ${\bar +}$ in such a way that ${\bar S}{\bar S}{\bar 0}{\bar +}{\bar S}{\bar S}{\bar S}{\bar 0}=_{ZF}{\bar S}{\bar S}{\bar S}{\bar S}{\bar S}{\bar 0}$ can be proven. All those sets (representing numbers) are then collected and put into a set $\mathbb N_{ZF}\equiv\{{\bar 0},{\bar S}{\bar 0},{\bar S}{\bar S}{\bar 0},\dots\}$ | In set theory, we can make //models// of other structures so that truths of their theories are reflected as truths of sets. For example, one commonly defines ${\bar 0}\equiv\{\}$, ${\bar S}x\equiv x\cup\{x\}$ and addition ${\bar +}$ in such a way that ${\bar S}{\bar S}{\bar 0}{\bar +}{\bar S}{\bar S}{\bar S}{\bar 0}=_{ZF}{\bar S}{\bar S}{\bar S}{\bar S}{\bar S}{\bar 0}$ can be proven. All those sets (representing numbers) are then collected and put into a set $\mathbb N_{ZF}\equiv\{{\bar 0},{\bar S}{\bar 0},{\bar S}{\bar S}{\bar 0},\dots\}$ | ||
| - | Another example is the model of the ordered pair $\langle x,y\rangle\equiv \{\{x\},\{x,y\}\}$ and then the following desired statement can be proven: $(\langle x,y\rangle=_{ZF}\langle u,v\rangle)\Leftrightarrow (x=_{ZF}u\land y=_{ZF}v)$. Furthermore, a group can be modeled as a pair $\langle G,*\rangle$, where is a set of group elements and $*$ is the function defining the multiplication table. Then the group $\mathbb Z_2$ of two elements can be presented as ${\mathrm z}_2^+\equiv\langle\{0,1\},+\rangle$ or ${\mathrm z}_2^\times\equiv\langle\{1,-1\},\times\rangle$, where $+$ is arithmetic addition mod $2$ and $\times$ is arithmetic multiplication. | + | Another example is the model of the ordered pair $\langle x,y\rangle\equiv \{\{x\},\{x,y\}\}$ and then the following desired statement can be proven: $(\langle x,y\rangle=_{ZF}\langle u,v\rangle)\Leftrightarrow (x=_{ZF}u\land y=_{ZF}v)$. Furthermore, a group can be modeled as a pair $\langle G,*\rangle$, where $G$ is a set of group elements and $*$ is the function defining the multiplication table. Then the group $\mathbb Z_2$ of two elements can be presented as ${\mathrm z}_2^+\equiv\langle\{0,1\},+\rangle$ or ${\mathrm z}_2^\times\equiv\langle\{1,-1\},\times\rangle$, where $+$ is arithmetic addition mod $2$ and $\times$ is arithmetic multiplication. |
| Because of its capacity to define models set theory can be taken as //foundation for mathematics//. One only needs <logic and set theory axioms and definition of concepts in terms of sets> as opposed to <logic and new axioms for each theory>. | Because of its capacity to define models set theory can be taken as //foundation for mathematics//. One only needs <logic and set theory axioms and definition of concepts in terms of sets> as opposed to <logic and new axioms for each theory>. | ||
| Line 47: | Line 47: | ||
| $Id_U(A,B)\simeq(A\simeq B)$ | $Id_U(A,B)\simeq(A\simeq B)$ | ||
| - | Here $\simeq$ is defined like a homotopy equivalence, in support of the $\infty$-groupoid pov. One could say that equality is dropped in favor of equivalence, however we keep the computational aspect. (141111 I'm not sure how the implementation of univalent foundation actually compares to properly weak higher category theory.) | + | Here $\simeq$ is defined like a homotopy equivalence, in support of the $\infty$-groupoid pov. (I've written down some explanations of the univalence axiom in the HoTT Wikipedia article.) |
| An isomorphism of a plain set is of course an invertible function - a bijection. Note that if by the set of natural numbers and set of rational numbers you merely mean the collection of their elements, then they are equal in HoTT (there is a bijection)! But as soon as you consider them equipped them with their structure (e.g. $+$ arithmetic), they are not equal. | An isomorphism of a plain set is of course an invertible function - a bijection. Note that if by the set of natural numbers and set of rational numbers you merely mean the collection of their elements, then they are equal in HoTT (there is a bijection)! But as soon as you consider them equipped them with their structure (e.g. $+$ arithmetic), they are not equal. | ||
