The Justification of Identity Elimination in Martin-Löf’s Type Theory

Topoi 38 (3):577-590 (2019)
  Copy   BIBTEX

Abstract

On the basis of Martin-Löf’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.

Categories

Keywords

Reprint years

DOI

10.1007/s11245-017-9509-1

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,100

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

On the strength of dependent products in the type theory of Martin-Löf.Richard Garner - 2009 - Annals of Pure and Applied Logic 160 (1):1-12.
Identity in Homotopy Type Theory: Part II, The Conceptual and Philosophical Status of Identity in HoTT.James Ladyman & Stuart Presnell - 2017 - Philosophia Mathematica 25 (2):210-245.
Cut-elimination for simple type theory with an axiom of choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
Cut-Elimination for Simple Type Theory with an Axiom of Choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
Identity in Homotopy Type Theory, Part I: The Justification of Path Induction.James Ladyman & Stuart Presnell - 2015 - Philosophia Mathematica 23 (3):386-406.
Proof-relevance of families of setoids and identity in type theory.Erik Palmgren - 2012 - Archive for Mathematical Logic 51 (1-2):35-47.
Saying 'I do' to identity.Richard Brown - manuscript
Homotopy theoretic models of identity types.Steve Awodey & Michael A. Warren - unknown
The Friedman‐Translation for Martin‐Löf's Type Theory.Erik Palmgren - 1995 - Mathematical Logic Quarterly 41 (3):314-326.
Type-identity conditions for phenomenal properties.Simone Gozzano - 2012 - In Simone Gozzano & Christopher S. Hill (eds.), New Perspective on Type Identity. The Mental and the Physical. Cambridge University Press. pp. 111-126.
Disappearance and the identity theory.Robert C. Richardson - 1981 - Canadian Journal of Philosophy 11 (September):473-85.
Categorical harmony and path induction.Patrick Walsh - 2017 - Review of Symbolic Logic 10 (2):301-321.
Belief from the Past.Andrew Naylor - 2010 - European Journal of Philosophy 20 (4):598-620.
The Generalised Type-Theoretic Interpretation of Constructive Set Theory.Nicola Gambino & Peter Aczel - 2006 - Journal of Symbolic Logic 71 (1):67 - 103.
An interpretation of Martin-löf's type theory in a type-free theory of propositions.Jan Smith - 1984 - Journal of Symbolic Logic 49 (3):730-753.

Analytics

Added to PP
2017-09-02

Downloads
56 (#286,455)

6 months
11 (#241,037)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Ansten Klev
Czech Academy of Sciences

Citations of this work

The Harmony of Identity.Ansten Klev - 2019 - Journal of Philosophical Logic 48 (5):867-884.
What Types Should Not Be.Bruno Bentzen - 2020 - Philosophia Mathematica 28 (1):60-76.
Identity in Martin‐Löf type theory.Ansten Klev - 2021 - Philosophy Compass 17 (2):e12805.
Identity in Martin‐Löf type theory.Ansten Klev - 2021 - Philosophy Compass 17 (2):e12805.

View all 7 citations / Add more citations

References found in this work

Natural deduction: a proof-theoretical study.Dag Prawitz - 1965 - Mineola, N.Y.: Dover Publications.
The iterative conception of set.George Boolos - 1971 - Journal of Philosophy 68 (8):215-231.
Natural Deduction: A Proof-Theoretical Study.Richmond Thomason - 1965 - Journal of Symbolic Logic 32 (2):255-256.
Ideas and Results in Proof Theory.Dag Prawitz & J. E. Fenstad - 1971 - Journal of Symbolic Logic 40 (2):232-234.

View all 19 references / Add more references