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

Authors
Bruno Bentzen
Carnegie Mellon University
Abstract
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.
Keywords Homotopy type theory  Type theory  Justification
Categories (categorize this paper)
DOI 10.1093/philmat/nkz014
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 54,646
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Grundlagen der Arithmetik.Gottlob Frege - 1884 - Breslau: Wilhelm Koebner Verlag.
The Iterative Conception of Set.George Boolos - 1971 - Journal of Philosophy 68 (8):215-231.
The Collected Papers of Gerhard Gentzen.Gerhard Gentzen - 1969 - Amsterdam: North-Holland Pub. Co..

View all 17 references / Add more references

Citations of this work BETA

On Different Ways of Being Equal.Bruno Bentzen - forthcoming - Erkenntnis:1-22.

Add more citations

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.
Concept Types and Determination.S. Lobner - 2011 - Journal of Semantics 28 (3):279-333.

Analytics

Added to PP index
2019-07-30

Total views
14 ( #668,401 of 2,385,991 )

Recent downloads (6 months)
3 ( #264,444 of 2,385,991 )

How can I increase my downloads?

Downloads

My notes