Eta-rules in Martin-Löf type theory

0510497 - FLÚ 2020 RIV US eng J - Journal Article
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
R&D Projects: GA ČR(CZ) GJ17-18344Y
Institutional support: RVO:67985955
Keywords : type theory * definitional identity
OECD category: Philosophy, History and Philosophy of science and technology
Impact factor: 0.406, year: 2019
Method of publishing: Limited access
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.
Permanent Link: http://hdl.handle.net/11104/0300973