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 14: | Line 14: | ||
In the following we outline why this is a good idea, if we want to use our type theory to formulate mathematics. | In the following we outline why this is a good idea, if we want to use our type theory to formulate mathematics. | ||
- | === Lengthy but necessary motivation === | + | === Motivation === |
== Theories and their equalities == | == Theories and their equalities == | ||
In equalitarian propositional logic, equality between two terms is a relation which per default is taken to be reflexive, symmetric and transitive. We can set up theories in logic (of numbers, of set elements, of group elements,...) and then further specify how to work with it via axioms. | In equalitarian propositional logic, equality between two terms is a relation which per default is taken to be reflexive, symmetric and transitive. We can set up theories in logic (of numbers, of set elements, of group elements,...) and then further specify how to work with it via axioms. | ||
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. |