Kuratowski finite sets in the UniMath Library

Title

Kuratowski finite sets in the UniMath Library

 Author

van de Laar, Luuk (TU Delft Electrical Engineering, Mathematics and Computer Science)

Contributor

Ahrens, B.P. (mentor)
Wullaert, K.F. (mentor)
Yorke-Smith, N. (graduation committee) ORCID 0000-0002-1814-3515

 Degree granting institution

Delft University of Technology

 Programme

Computer Science and Engineering

 Project

CSE3000 Research Project

 Date

2023-06-28

 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.

 Subject

HoTT
UniMath
Kuratowski Finite
Coq
Proof assistant

 To reference this document use:

http://resolver.tudelft.nl/uuid:d30b490a-b4b4-4e97-b4b8-ea89a2addcdd

 Part of collection

Student theses

 Document type

bachelor thesis

 Rights

© 2023 Luuk van de Laar
Files
PDF CSE3000_Final_Paper_Final ... sion_3.pdf 190.59 KB
Close viewer