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 JanDisplayed time zone: Tijuana, Baja California change

 13:30 - 15:30 Type Theory, Set Theory, and Formalized MathematicsCPP at Museum A Chair(s): Thorsten Altenkirch University of Nottingham 13:3030mTalk Finite Sets in Homotopy Type TheoryCPPDan Frumin Radboud University, Herman Geuvers Radboud University Nijmegen, Netherlands, Léon Gondelman LRI, Université Paris-Sud, Niels van der Weide Radboud University Nijmegen, Netherlands DOI 14:0030mTalk Generic Derivation of Induction for Impredicative Encodings in CedilleCPPDenis Firsov University of Iowa, USA, Aaron Stump University of Iowa, USA DOI 14:3030mTalk Large Model Constructions for Second-Order ZF in Dependent Type TheoryCPPDominik Kirst Saarland University, Gert Smolka Saarland University DOI 15:0030mTalk A Constructive Formalisation of Semi-algebraic Sets and FunctionsCPPBoris Djalal INRIA