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