# Finite Sets in Homotopy Type Theory

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).

## Preprint

The preprint version of the paper can be found here.

## Source code

The artifact with the source code corresponding to the development in the paper can be downloaded here: artifact.tgz.

It contains

- The source code containing formalized proofs for all the propositions in the paper and more.
- The HoTT Coq library version f7373188e9ed08046f43ebf72cd52dfe4e1721bf (it is known that the artifact can be compiled against that version of HoTT).

See the `FiniteSets/CPP.v`

file for an overview linking the statements in the paper to the propositions in the Coq formalization.

### Building instructions

(Tested with Coq 8.6)

- Compile the HoTT library. See
`HoTT/INSTALL.md`

for detailed instructions.
- Make sure that
`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
make
```

## Development version

The latest version of the source code can be found on Github.