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 $\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'' and
Kuratowski-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:30 30mTalk | 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 30mTalk | Generic Derivation of Induction for Impredicative Encodings in Cedille CPP DOI | ||
14:30 30mTalk | Large Model Constructions for Second-Order ZF in Dependent Type Theory CPP DOI | ||
15:00 30mTalk | A Constructive Formalisation of Semi-algebraic Sets and Functions CPP Boris Djalal INRIA |