Evaluating Scopes of Different Implementations of Finite Sets in Homotopy Type Theory
G. Fincato de Loureiro (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 report explores the differences in implementations of homotopy type theory using different definitions of finite sets. The expressive ability of homotopy theory is explored when using the newly established definition and implementation of Kuratowski finite sets. This implementation is then compared to that when using the previously established definition and implementation of Bishop finite sets in homotopy type theory. The implementation of finite sets in homotopy type theory is a topic of extensive research. Recent advances have come up with an implementation of Kuratowski-finite sets which promises to be more general and flexible than previously established implementations of finite sets via Bishop-finite sets and enumerated types. This paper will explore examples of types that satisfy Kuratowki-finite notions of finite sets, but not Bishop-finite notions. Through these examples, it will be proven that Kuratowski-finite notions are strictly more flexible than Bishop-finite notions. It will then be proven that by using Kuratowski-notions, the familiar computations involving sets can be used in the same way as with Bishop-finite sets; there is no loss in computational facilities