Počet záznamů: 1
Eta-rules in Martin-Löf type theory
- 1.
SYSNO ASEP 0510497 Druh ASEP J - Článek v odborném periodiku Zařazení RIV J - Článek v odborném periodiku Poddruh J Článek ve WOS Název Eta-rules in Martin-Löf type theory Tvůrce(i) Klev, Ansten (FLU-F) ORCID, RID, SAI Zdroj.dok. Bulletin of Symbolic Logic. - : Cambridge University Press - ISSN 1079-8986
Roč. 25, č. 3 (2019), s. 333-359Poč.str. 27 s. Forma vydání Tištěná - P Jazyk dok. eng - angličtina Země vyd. US - Spojené státy americké Klíč. slova type theory ; definitional identity Vědní obor RIV AA - Filosofie a náboženství Obor OECD Philosophy, History and Philosophy of science and technology CEP GJ17-18344Y GA ČR - Grantová agentura ČR Způsob publikování Omezený přístup Institucionální podpora FLU-F - RVO:67985955 UT WOS 000510726600003 EID SCOPUS 85074250338 DOI 10.1017/bsl.2019.21 Anotace 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. Pracoviště Filosofický ústav Kontakt Chlumská Simona, chlumska@flu.cas.cz ; Tichá Zuzana, asep@flu.cas.cz Tel: 221 183 360 Rok sběru 2020 Elektronická adresa https://www.cambridge.org/core/journals/bulletin-of-symbolic-logic/article/etarules-in-martinlof-type-theory/CA10751125AABA4B36BEDC30EC729B74
Počet záznamů: 1