Identity in Martin‐Löf type theory

Philosophy Compass 17 (2):e12805 (2021)
  Copy   BIBTEX

Abstract

Philosophy Compass, Volume 17, Issue 2, February 2022.

Categories

Keywords

Reprint years

2022

DOI

10.1111/phc3.12805

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,846

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

The Justification of Identity Elimination in Martin-Löf’s Type Theory.Ansten Klev - 2019 - Topoi 38 (3):577-590.
Identity in Martin‐Löf type theory.Ansten Klev - 2021 - Philosophy Compass 17 (2):e12805.
Eta-rules in Martin-löf type theory.Ansten Klev - 2019 - Bulletin of Symbolic Logic 25 (3):333-359.
A Comparison of Type Theory with Set Theory.Ansten Klev - 2019 - In Deniz Sarikaya, Deborah Kant & Stefania Centrone (eds.), Reflections on the Foundations of Mathematics. Springer Verlag. pp. 271-292.
A Comparison of Type Theory with Set Theory.Ansten Klev - 2019 - In Stefania Centrone, Deborah Kant & Deniz Sarikaya (eds.), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts. Springer Verlag. pp. 271-292.
Mind-body identity revised.Chenyang Li - 1994 - Philosophia 24 (1-2):105-114.
Proof-relevance of families of setoids and identity in type theory.Erik Palmgren - 2012 - Archive for Mathematical Logic 51 (1-2):35-47.
Identity and Sortals.Ansten Klev - 2017 - Erkenntnis 82 (1):1-16.
Saying 'I do' to identity.Richard Brown - manuscript
The Friedman‐Translation for Martin‐Löf's Type Theory.Erik Palmgren - 1995 - Mathematical Logic Quarterly 41 (3):314-326.
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.
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.
Homotopy theoretic models of identity types.Steve Awodey & Michael A. Warren - unknown
New Perspectives on Type Identity: The Mental and the Physical.Simone Gozzano & Christopher S. Hill (eds.) - 2012 - Cambridge: Cambridge University Press.

Analytics

Added to PP
2022-02-25

Downloads
19 (#798,463)

6 months
7 (#428,584)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Ansten Klev
Czech Academy of Sciences

Citations of this work

Constructive Type Theory, an appetizer.Laura Crosilla - 2024 - In Peter Fritz & Nicholas K. Jones (eds.), Higher-Order Metaphysics. Oxford University Press.

Add more citations

References found in this work

A formulation of the simple theory of types.Alonzo Church - 1940 - Journal of Symbolic Logic 5 (2):56-68.
Begriffsschrift.Gottlob Frege - 1967 - In Jean Van Heijenoort (ed.), From Frege to Gödel. Cambridge: Harvard University Press. pp. 1-83.
Structuralism, Invariance, and Univalence.Steve Awodey - 2014 - Philosophia Mathematica 22 (1):1-11.

View all 33 references / Add more references