Evaluating Scopes of Different Implementations of Finite Sets in Homotopy Type Theory

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