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 $\mathcal{K}(A)$ of ``finite sets over type $A$'' \emph{à la} Kuratowski
without assuming that $\mathcal{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.

On the foundational side, we use $\mathcal{K}$ to define the notions of
Kuratowski-finite type'' andKuratowski-finite subobject'', which we contrast with
established notions, \eg 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 $\mathcal{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 $\mathcal{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 $\mathcal{K}(A)$.

Tue 9 Jan
Times are displayed in time zone: (GMT-07:00) Tijuana, Baja California change

CPP-2018
13:30 - 15:30: CPP 2018 - Type Theory, Set Theory, and Formalized Mathematics at Museum A
Chair(s): Thorsten AltenkirchUniversity of Nottingham
CPP-201813:30 - 14:00
Talk
Dan FruminRadboud University, Herman GeuversRadboud University Nijmegen, Netherlands, Léon GondelmanLRI, Université Paris-Sud, Niels van der WeideRadboud University Nijmegen, Netherlands
DOI
CPP-201814:00 - 14:30
Talk
Denis FirsovUniversity of Iowa, USA, Aaron StumpUniversity of Iowa, USA
DOI
CPP-201814:30 - 15:00
Talk
Dominik KirstSaarland University, Gert SmolkaSaarland University
DOI
CPP-201815:00 - 15:30
Talk