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.
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

237 (#55,242)

6 months
111 (#10,133)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Bruno Bentzen
Zhejiang University

Citations of this work

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

Add more citations