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

Kód výsledku v 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>
Výsledek na webu
<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>

Jazyk výsledku
angličtina
Název v původním jazyce
The Justification of Identity Elimination in Martin-Lof’s Type Theory
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
The Justification of Identity Elimination in Martin-Lof’s Type Theory
Popis výsledku anglicky
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.

Druh
J<sub>imp</sub> - Článek v periodiku v databázi Web of Science
CEP obor
—
OECD FORD obor
60301 - Philosophy, History and Philosophy of science and technology

Projekt
<a href="/cs/project/GJ17-18344Y" target="_blank" >GJ17-18344Y: Logicko-filozofická analýza pojmu identity</a><br>
Návaznosti
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění
2019
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Podobné výsledky(10)