Number of the records: 1
The Justification of Identity Elimination in Martin-Lof’s Type Theory
- 1.0508058 - FLÚ 2020 RIV NL eng J - Journal Article
Klev, Ansten
The Justification of Identity Elimination in Martin-Lof’s Type Theory.
Topoi: an international review of philosophy. Roč. 38, č. 3 (2019), s. 577-590. ISSN 0167-7411
R&D Projects: GA ČR(CZ) GJ17-18344Y
Institutional support: RVO:67985955
Keywords : Justification of logical laws * Type theory * Identity
OECD category: Philosophy, History and Philosophy of science and technology
Method of publishing: Limited access
https://link.springer.com/article/10.1007%2Fs11245-017-9509-1
On the basis of Martin-Lof’s meaning explanations for his type theory a detailed justification is offered of the rule of identity elimination. Brief discussions are thereafter offered of how the univalence axiom fares with respect to these meaning explanations and of some recent work on identity in type theory by Ladyman and Presnell.
Permanent Link: http://hdl.handle.net/11104/0299265
Number of the records: 1