Constructive mathematics and equality

Dissertation, Sun Yat-Sen University (2018)

Bruno Bentzen
Carnegie Mellon University
The aim of the present thesis is twofold. First we propose a constructive solution to Frege's puzzle using an approach based on homotopy type theory, a newly proposed foundation of mathematics that possesses a higher-dimensional treatment of equality. We claim that, from the viewpoint of constructivism, Frege's solution is unable to explain the so-called ‘cognitive significance' of equality statements, since, as we shall argue, not only statements of the form 'a = b', but also 'a = a' may contribute to an extension of knowledge. Second, we study this higher-dimensional account of equality from a constructive (computational) standpoint and, based on these considerations, we offer a new perspective to the project proposed by Peter Aczel of developing conventions and notations for an informal style of doing mathematics in type theory. To that end, we adopt the cubical type theory of Angiuli, Favonia and Harper, a framework that can be seen as constructive refinement of the ideas of homotopy type theory.
Keywords Homotopy type theory  Frege's puzzle  Cubical type theory  Equality
Categories (categorize this paper)
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,491
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

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Does Homotopy Type Theory Provide a Foundation for Mathematics?James Ladyman & Stuart Presnell - 2016 - British Journal for the Philosophy of Science:axw006.
What Types Should Not Be.Bruno Bentzen - 2020 - Philosophia Mathematica 28 (1):60-76.
Structuralism, Invariance, and Univalence.Steve Awodey - 2014 - Philosophia Mathematica 22 (1):1-11.
A Minimalist Two-Level Foundation for Constructive Mathematics.Maria Emilia Maietti - 2009 - Annals of Pure and Applied Logic 160 (3):319-354.
Constructive Notions of Set: Part I. Sets in Martin–Löf Type Theory.Laura Crosilla - 2005 - Annali Del Dipartimento di Filosofia 11:347-387.
Models of HoTT and the Constructive View of Theories.Andrei Rodin - 2019 - In Deniz Sarikaya, Deborah Kant & Stefania Centrone (eds.), Reflections on the Foundations of Mathematics. Springer Verlag.
The Strength of Some Martin-Löf Type Theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.


Added to PP index

Total views

Recent downloads (6 months)

How can I increase my downloads?


Sorry, there are not enough data points to plot this chart.

My notes