Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
univalence_axiom [2014/11/18 13:29] nikolaj |
univalence_axiom [2014/11/18 13:30] nikolaj |
||
|---|---|---|---|
| Line 10: | Line 10: | ||
| RHS: Here the [[type equivalence]] $(A\simeq B)$ is defined in terms of functions running in opposite directions, $A\to B$ and $B\to A$. | RHS: Here the [[type equivalence]] $(A\simeq B)$ is defined in terms of functions running in opposite directions, $A\to B$ and $B\to A$. | ||
| - | Per definition, the identity type $Id_U(A,A)$ is inhabited by the term $refl_A$ and this corresponds to the (invertible) identity function $id_A:A\to A$. Now more generally, adding the univalence axiom gives means to the identity type of the theory by "filling it up" with functions from the type of equivalences. In other words, what's relevant is the corrolary "$(A\simeq B)\to Id_U(A,B)$ ... is inhabited". | + | Per definition, the identity type $Id_U(A,A)$ is inhabited by the term $refl_A$ and this corresponds to the (invertible) identity function $id_A:A\to A$. Now more generally, adding the univalence axiom gives means to the identity type of the theory by "filling it up" with functions from the type of equivalences. In other words, what's relevant is the corrolary "there is a function of type $(A\simeq B)\to Id_U(A,B)$". |
| 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. | ||
