Eta-rules in Martin-Löf type theory
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Eta-rules in Martin-Löf type theory
Original language description
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.
Czech name
—
Czech description
—
Classification
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
Result continuities
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
Others
Publication year
2019
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Bulletin of Symbolic Logic
ISSN
1079-8986
e-ISSN
—
Volume of the periodical
25
Issue of the periodical within the volume
3
Country of publishing house
US - UNITED STATES
Number of pages
27
Pages from-to
333-359
UT code for WoS article
000510726600003
EID of the result in the Scopus database
2-s2.0-85074250338