What Types Should Not Be

Philosophia Mathematica 28 (1):60-76 (2020)
  Copy   BIBTEX


In a series of papers Ladyman and Presnell raise an interesting challenge of providing a pre-mathematical justification for homotopy type theory. In response, they propose what they claim to be an informal semantics for homotopy type theory where types and terms are regarded as mathematical concepts. The aim of this paper is to raise some issues which need to be resolved for the successful development of their types-as-concepts interpretation.

Similar books and articles

Universes and univalence in homotopy type theory.James Ladyman & Stuart Presnell - 2019 - Review of Symbolic Logic 12 (3):426-455.
Does Homotopy Type Theory Provide a Foundation for Mathematics?James Ladyman & Stuart Presnell - 2016 - British Journal for the Philosophy of Science:axw006.
Identity in HoTT, Part I.James Ladyman & Stuart Presnell - 2015 - Philosophia Mathematica 23 (3):386-406.
Prototype Proofs in Type Theory.Giuseppe Longo - 2000 - Mathematical Logic Quarterly 46 (2):257-266.
Abstract Data Types and Type Theory: Theories as Types.Ruy J. B. de Queiroz - 1991 - Mathematical Logic Quarterly 37 (9-12):149-166.


Added to PP

468 (#39,082)

6 months
124 (#27,465)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Bruno Bentzen
Zhejiang University

Citations of this work

Sense, reference, and computation.Bruno Bentzen - 2020 - Perspectiva Filosófica 47 (2):179-203.
On Different Ways of Being Equal.Bruno Bentzen - 2020 - Erkenntnis 87 (4):1809-1830.

Add more citations

References found in this work

Constructivism in mathematics: an introduction.A. S. Troelstra - 1988 - New York, N.Y.: Sole distributors for the U.S.A. and Canada, Elsevier Science Pub. Co.. Edited by D. van Dalen.
The collected papers of Gerhard Gentzen.Gerhard Gentzen - 1969 - Amsterdam,: North-Holland Pub. Co.. Edited by M. E. Szabo.

View all 21 references / Add more references