The Justification of Identity Elimination in Martin-Lof’s Type Theory

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985955%3A_____%2F19%3A00508058" target="_blank" >RIV/67985955:_____/19:00508058 - isvavai.cz</a>
Result on the web
<a href="https://link.springer.com/article/10.1007%2Fs11245-017-9509-1" target="_blank" >https://link.springer.com/article/10.1007%2Fs11245-017-9509-1</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/s11245-017-9509-1" target="_blank" >10.1007/s11245-017-9509-1</a>

Result language
angličtina
Original language name
The Justification of Identity Elimination in Martin-Lof’s Type Theory
Original language description
On the basis of Martin-Lof’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.
Czech name
—
Czech description
—

Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
60301 - Philosophy, History and Philosophy of science and technology

Project
<a href="/en/project/GJ17-18344Y" target="_blank" >GJ17-18344Y: A logico-philosophical analysis of the notion of identity</a><br>
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year
2019
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)