Quotients, inductive types, and quotient inductive types

Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp

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 ind…