Kuratowski finite sets in the UniMath Library

Bachelor thesis (2023)

Authors

L.W.L. van de Laar Electrical Engineering, Mathematics and Computer Science

Contributors

B.P. Ahrens Programming Languages - EEMCS (mentor)
K.F. Wullaert Programming Languages - EEMCS (mentor)
N. Yorke-Smith Algorithmics - EEMCS (graduation committee member)
Faculty
Electrical Engineering, Mathematics and Computer Science, Electrical Engineering, Mathematics and Computer Science
Copyright: © 2023 Luuk van de Laar
More Info
expand_more

Published Date

28-06-2023

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 focuses on implementing and verifying the proofs presented in ``Finite Sets in Homotopy Type Theory" within the UniMath library. The UniMath library currently lacks support for higher inductive types, which are crucial for reasoning about finite sets in Homotopy Type Theory. This paper addresses that issue and introduces higher inductive types to UniMath. This is used to develop a computer-checked implementation of the proofs within "Finite Sets in Homotopy Type Theory." This implementation enables future research on finite sets in HoTT by providing accessible and reliable proofs.

This paper defines finite sets as Kuratowski-finite. This is in contrast with the most common notion of finiteness, e.g. Bishop-finite and enumerated types. I argue that Kuratowski-finiteness is the most general finite for which the usual operations of finite types and sub-objects can be operated upon.