# Defining Functions on Equivalence Classes

## TL;DR

This paper presents techniques for defining and reasoning about quotient types, which are abstract types formed by equivalence classes, with applications to defining integers from natural numbers and recursive datatypes.

## Contribution

It introduces simple, general methods for working with quotient constructions and equivalence classes, supported by a lemma library, with practical applications.

## Key findings

- Techniques for defining quotient types using equivalence relations
- Application of methods to define integers from natural numbers
- Application to recursive datatypes with equational constraints

## Abstract

A quotient construction defines an abstract type from a concrete type, using an equivalence relation to identify elements of the concrete type that are to be regarded as indistinguishable. The elements of a quotient type are \emph{equivalence classes}: sets of equivalent concrete values. Simple techniques are presented for defining and reasoning about quotient constructions, based on a general lemma library concerning functions that operate on equivalence classes. The techniques are applied to a definition of the integers from the natural numbers, and then to the definition of a recursive datatype satisfying equational constraints.