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

Displayed 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:30
30m
Talk
Finite Sets in Homotopy Type Theory
CPP
Dan 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:00
30m
Talk
Generic Derivation of Induction for Impredicative Encodings in Cedille
CPP
Denis Firsov University of Iowa, USA, Aaron Stump University of Iowa, USA
DOI
14:30
30m
Talk
Large Model Constructions for Second-Order ZF in Dependent Type Theory
CPP
Dominik Kirst Saarland University, Gert Smolka Saarland University
DOI
15:00
30m
Talk
A Constructive Formalisation of Semi-algebraic Sets and Functions
CPP