Finite sets in homotopy type theory
Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide · 2018
We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type K(A) of "finite sets over type A" à la Kuratowski without assuming that K(A) has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition.