Univalent foundations as structuralist foundations
type: Item
instance of: scholarly article
title: Univalent foundations as structuralist foundations
zbMATH Open document ID: 1400.03023
author: Dimitris Tsementzis
published in: Synthese
publication date: 2018-03-27T00:00:00Z
full work available at URL: UF.asSF.finaldraft.pdf
review text: Univalent foundations (UF), which grew out of homotopy-theoretic models of Martin-Löf type theory, replace sets with homotopy types as fundamental objects. In the paper under review, the author argues that UF may provide a suitable formalisation of the structuralist approach to mathematics. To this aim, he formulates a criterion that a foundation is required to satisfy to be identified as structuralist, namely that, for any branch of mathematics, the expressible properties should be invariant under the relevant criterion of identity. For example, in group theory the properties that our formal system allows us to formulate should be invariant under isomorphism. The author then explains how both Zermelo-Fraenkel set theory and the elementary theory of the category of sets fail to meet this requirement. The more technical part of the paper is devoted to arguing that UF do allow a faithful formalisation of the concept of ``relevant criterion of identity'' under which all well-formed predicates are invariant. The last section discusses and counters three arguments against the role of UF as a foundation for the whole of mathematics (a so-called ``big-f'' foundation).
reviewed by: Jacopo Emmenegger
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 03A05
Mathematics Subject Classification ID: 03B30
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 18A15
Mathematics Subject Classification ID: 55U40
zbMATH DE Number: 6853130
zbMATH Keywords: structuralism
zbMATH Keywords: foundations of mathematics
zbMATH Keywords: univalent foundations
describes a project that uses: cubicaltt
MaRDI profile type: Publication
OpenAlex ID: W2395479267
cites work: Univalent categories and the Rezk completion
cites work: An Answer to Hellman's Question: ‘Does Category Theory Provide a Framework for Mathematical Structuralism?’†
cites work: Structuralism, Invariance, and Univalence
cites work: Homotopy theoretic models of identity types
cites work: Q2968413
cites work: Équivalence naturelle et formules logiques en théorie des catégories
cites work: Cubical Type Theory: a constructive interpretation of the univalence axiom
cites work: Q4109809
cites work: Kant on geometry and spatial intuition
cites work: Q4364755
cites work: Three varieties of mathematical structuralism
cites work: Q4247303
cites work: Mathematical forms and forms of mathematics: leaving the shores of extensional mathematics
cites work: Q3986540
cites work: Rethinking Set Theory
cites work: Q4679166
cites work: Higher Topos Theory (AM-170)
cites work: Q4381416
cites work: CATEGORICAL FOUNDATIONS OF MATHEMATICS OR HOW TO PROVIDE FOUNDATIONS FORABSTRACTMATHEMATICS
cites work: Q3688389
cites work: Numbers Can Be Just What They Have To
cites work: Exploring Categorical Structuralism
cites work: A lattice of interpretability types of theories
cites work: Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets
cites work: The structuralist view of mathematical objects
cites work: Mathematics as a Science of Patterns: Ontology and Reference
cites work: Quantum Gauge Field Theory in Cohesive Homotopy Type Theory
cites work: Q4388801
cites work: Brouwer's fixed-point theorem in real-cohesive homotopy type theory
cites work: What is a Higher-Level Set?
cites work: An experimental library of formalized Mathematics based on the univalent foundations
DOI: 10.1007/S11229-016-1109-X
description: scientific article; zbMATH DE number 6853130