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 | ||
|
univalence_axiom [2014/11/18 13:30] nikolaj |
univalence_axiom [2016/07/18 00:27] 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 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. | ||
