Eta-rules in Martin-Löf type theory

0510497 - FLÚ 2020 RIV US eng J - Článek v odborném periodiku
Klev, Ansten
Eta-rules in Martin-Löf type theory.
Bulletin of Symbolic Logic. Roč. 25, č. 3 (2019), s. 333-359. ISSN 1079-8986. E-ISSN 1943-5894
Grant CEP: GA ČR(CZ) GJ17-18344Y
Institucionální podpora: RVO:67985955
Klíčová slova: type theory * definitional identity
Obor OECD: Philosophy, History and Philosophy of science and technology
Impakt faktor: 0.406, rok: 2019
Způsob publikování: Omezený přístup
https://www.cambridge.org/core/journals/bulletin-of-symbolic-logic/article/etarules-in-martinlof-type-theory/CA10751125AABA4B36BEDC30EC729B74

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.
Trvalý link: http://hdl.handle.net/11104/0300973