Quotients, inductive types, and quotient inductive types

TL;DR

This paper introduces quotient-inductive types (QWI types) in constructive type theory, showing they can be derived from quotient and inductive types under certain conditions, with formal verification in Agda.

Contribution

It defines QWI types as initial algebras for indexed equational theories and demonstrates their derivation from existing types using the WISC axiom.

Findings

QWI types can be constructed as colimits of approximations.

The construction relies on the WISC axiom.

Formal proof verified in Agda.

Abstract

This paper introduces an expressive class of indexed quotient-inductive types, called QWI types, within the framework of constructive type theory. They are initial algebras for indexed families of equational theories with possibly infinitary operators and equations. We prove that QWI types can be derived from quotient types and inductive types in the type theory of toposes with natural number object and universes, provided those universes satisfy the Weakly Initial Set of Covers (WISC) axiom. We do so by constructing QWI types as colimits of a family of approximations to them defined by well-founded recursion over a suitable notion of size, whose definition involves the WISC axiom. We developed the proof and checked it using the Agda theorem prover.