Quotients for Enumerable Types
Lulof Pirée
Tallinn University of Technology
Abstract:
Quotients are ubiquitous in classical mathematics,
but difficult to implement constructively in intensional dependent type theory.
However, we found a straightforward recipe for constructing quotients
over any enumerable type.
This construction exploits the fact that equivalence relations over such types
can be encoded as normalisation functions.
Many well-known data types are enumerable, including trees, strings,
lists of numbers, etc.
More generally, we identify the class of enumerable inductive types with
'signatures' and give a generic enumeration algorithm for them;
making them available to be quotiented.
This talk explains the ideas from a combinatorial angle,
and should be understandable without familiarity with the syntax of dependent
type theory.
All results have been formalised in Agda, see https://nifrec.github.io/eser-doc/
for clickable documentation or https://github.com/Nifrec/eser for the source code.