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 A has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition.
On the foundational side, we use K(-) to define the notions of "Kuratowski-finite type" and "Kuratowski-finite subobject", which we contrast with established notions, e.g. Bishop-finite types and enumerated types. We argue that Kuratowski-finiteness is the most general and flexible one of those and we define the usual operations on finite types and subobjects.
From the computational perspective, we show how to use K(A) for an abstract interface for well-known finite set implementations such as tree- and list-like data structures. This implies that a function defined on a concrete finite sets implementation can be obtained from a function defined on the abstract finite sets K(A) and that correctness properties are inherited. Hence, HoTT is the ideal setting for data refinement. Beside this, we define bounded quantification, which lifts a decidable property on A to one on K(A).
The preprint version of the paper can be found here.
The artifact with the source code corresponding to the development in the paper can be downloaded here: artifact.tgz.
It contains
See the FiniteSets/CPP.v file for an overview linking the statements in the paper to the propositions in the Coq formalization.
(Tested with Coq 8.6)
HoTT/INSTALL.md for detailed instructions.hoqc is in your $PATH, e.g. by executing export PATH=(path_to_the_HoTT_directory):$PATH in bash.Generate the Makefile in the FiniteSets directory and compile the code:
coq_makefile -f _CoqProject -o Makefile
makeThe latest version of the source code can be found on Github.