The Justification of Identity Elimination in Martin-Löf's Type Theory.
On the basis of Martin-Löf's meaning explanations for his type theory a detailed justification is offered of the rule of identity elimination. Brief discussions are thereafter offered of how the univalence axiom fares with respect to these meaning explanations and of some recent work on identity in...
| Publicado en: | Topoi: An International Review of Philosophy Vol. 38; no. 3; pp. 577 - 591 |
|---|---|
| Autor principal: | |
| Formato: | Artículo |
| Publicado: |
Springer Nature
Sep2019
|
| Materias: | |
| Acceso en línea: | Ver este registro en EBSCOhost |
| Sumario: | On the basis of Martin-Löf's meaning explanations for his type theory a detailed justification is offered of the rule of identity elimination. Brief discussions are thereafter offered of how the univalence axiom fares with respect to these meaning explanations and of some recent work on identity in type theory by Ladyman and Presnell. |
|---|