The Category of Sets in Homotopy Type Theory

More Info


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.