Eta-rules in Martin-Löf type theory

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985955%3A_____%2F19%3A00510497" target="_blank" >RIV/67985955:_____/19:00510497 - isvavai.cz</a>

Výsledek na webu

<a href="https://www.cambridge.org/core/journals/bulletin-of-symbolic-logic/article/etarules-in-martinlof-type-theory/CA10751125AABA4B36BEDC30EC729B74" target="_blank" >https://www.cambridge.org/core/journals/bulletin-of-symbolic-logic/article/etarules-in-martinlof-type-theory/CA10751125AABA4B36BEDC30EC729B74</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1017/bsl.2019.21" target="_blank" >10.1017/bsl.2019.21</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Eta-rules in Martin-Löf type theory

Popis výsledku v původním jazyce

The eta rule for a set A says that an arbitrary element of A is judgementally identical to an element of constructor form. Eta rules are not part of what may be called canonical Martin-Löf type theory. They are, however, justified by the meaning explanations, and a higher order eta rule is part of that type theory. The main aim of this article is to clarify this somewhat puzzling situation. It will be argued that lower order eta rules do not, whereas the higher order eta rule does, accord with the understanding of judgemental identity as definitional identity. A subsidiary aim is to clarify precisely what an eta rule is. This will involve showing how such rules relate to various other notions of type theory, proof theory, and category theory.

Název v anglickém jazyce

Eta-rules in Martin-Löf type theory

Popis výsledku anglicky

The eta rule for a set A says that an arbitrary element of A is judgementally identical to an element of constructor form. Eta rules are not part of what may be called canonical Martin-Löf type theory. They are, however, justified by the meaning explanations, and a higher order eta rule is part of that type theory. The main aim of this article is to clarify this somewhat puzzling situation. It will be argued that lower order eta rules do not, whereas the higher order eta rule does, accord with the understanding of judgemental identity as definitional identity. A subsidiary aim is to clarify precisely what an eta rule is. This will involve showing how such rules relate to various other notions of type theory, proof theory, and category theory.

Druh

J_imp - Č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ů

Název periodika

Bulletin of Symbolic Logic

ISSN

1079-8986

e-ISSN

—

Svazek periodika

25

Číslo periodika v rámci svazku

3

Stát vydavatele periodika

US - Spojené státy americké

Počet stran výsledku

27

Strana od-do

333-359

Kód UT WoS článku

000510726600003

EID výsledku v databázi Scopus

2-s2.0-85074250338