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&#39;&#39; 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

 13:30 - 15:30: CPP 2018 - Type Theory, Set Theory, and Formalized Mathematics at Museum A Chair(s): Thorsten AltenkirchUniversity of Nottingham 13:30 - 14:00Talk Finite Sets in Homotopy Type TheoryDan FruminRadboud University, Herman GeuversRadboud University Nijmegen, Netherlands, Léon GondelmanLRI, Université Paris-Sud, Niels van der WeideRadboud University Nijmegen, Netherlands DOI 14:00 - 14:30Talk Generic Derivation of Induction for Impredicative Encodings in CedilleDenis FirsovUniversity of Iowa, USA, Aaron StumpUniversity of Iowa, USA DOI 14:30 - 15:00Talk Large Model Constructions for Second-Order ZF in Dependent Type TheoryDominik KirstSaarland University, Gert SmolkaSaarland University DOI 15:00 - 15:30Talk A Constructive Formalisation of Semi-algebraic Sets and FunctionsBoris DjalalINRIA