PhilSci Archive

Univalent Foundations as a Foundation for Mathematical Practice

Crane, Harry (2018) Univalent Foundations as a Foundation for Mathematical Practice. [Preprint]


Download (452kB) | Preview


I prove that invoking the univalence axiom is equivalent to arguing 'without loss of generality' (WLOG) within Propositional Univalent Foundations (PropUF), the fragment of Univalent Foundations (UF) in which all homotopy types are mere propositions. As a consequence, I argue that practicing mathematicians, in accepting WLOG as a valid form of argument, implicitly accept the univalence axiom and that UF rightly serves as a Foundation for Mathematical Practice. By contrast, ZFC is inconsistent with WLOG as it is commonly applied, and therefore cannot serve as a foundation for practice.

Export/Citation: EndNote | BibTeX | Dublin Core | ASCII/Text Citation (Chicago) | HTML Citation | OpenURL
Social Networking:
Share |

Item Type: Preprint
Keywords: Univalent Foundations, univalence axiom, foundations of mathematics, set theory, ZFC, without loss of generality, mathematical practice
Subjects: Specific Sciences > Mathematics
Depositing User: Harry Crane
Date Deposited: 26 Aug 2018 19:06
Last Modified: 26 Aug 2018 19:06
Item ID: 14966
Subjects: Specific Sciences > Mathematics
Date: 14 August 2018

Monthly Views for the past 3 years

Monthly Downloads for the past 3 years

Plum Analytics

Actions (login required)

View Item View Item