The Category of Sets in Homotopy Type Theory
H. Lixandru (TU Delft - Electrical Engineering, Mathematics and Computer Science)
K.F. Wullaert – Mentor (TU Delft - Programming Languages)
Benedikt Ahrens – Mentor (TU Delft - Programming Languages)
Rihan Hai – Graduation committee member (TU Delft - Web Information Systems)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
This paper is a literature survey on homotopy type theory, analyzing the formalization of sets within homotopy type theory. Set theory is embedded in homotopy type theory via h-sets, with all h-sets forming the type Set. This paper presents the properties of the type Set from a categorical perspective, comparing it with its set-theoretic counterpart. We will also compare homotopy type theory to standard axiomatic set theory from the point of view of mathematical foundations, discussing the axiom of the empty set, the power set axiom and the axiom of choice and their equivalents in homotopy type theory.