The Category of Sets in Homotopy Type Theory

Bachelor thesis (2022)

Authors

H. Lixandru Electrical Engineering, Mathematics and Computer Science

Contributors

K.F. Wullaert Programming Languages - EEMCS (mentor)
B.P. Ahrens Programming Languages - EEMCS (mentor)
R. Hai Web Information Systems - EEMCS (graduation committee member)
Faculty
Electrical Engineering, Mathematics and Computer Science, Electrical Engineering, Mathematics and Computer Science
Copyright: © 2022 Horia Lixandru
More Info
expand_more

Published Date

22-06-2022

Language

English

Reuse Rights

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.

Faculty

Electrical Engineering, Mathematics and Computer Science

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.