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

Preview

Text univalence-4.pdf Download (452kB) | Preview

Abstract

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
Creators:	Creators Email ORCID Crane, Harry hcrane@stat.rutgers.edu
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
URI:	https://philsci-archive.pitt.edu/id/eprint/14966

Monthly Views for the past 3 years

Monthly Downloads for the past 3 years

Plum Analytics

Actions (login required)

View Item