Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next 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. | ||
| - | === 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. | ||
