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.
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.mdfor detailed instructions.
hoqcis in your
$PATH, e.g. by executing
export PATH=(path_to_the_HoTT_directory):$PATHin bash.
Generate the Makefile in the
FiniteSets directory and compile the code:
coq_makefile -f _CoqProject -o Makefile make
The latest version of the source code can be found on Github.