Quotients, inductive types, and quotient inductive types

This paper introduces an expressive class of indexed quotient-inductivetypes, called QWI types, within the framework of constructive type theory. Theyare initial algebras for indexed families of equational theories with possiblyinfinitary operators and equations. We prove that QWI types can be derived fromquotient types and inductive types in the type theory of toposes with naturalnumber object and universes, provided those universes satisfy the WeaklyInitial Set of Covers (WISC) axiom. We do so by constructing QWI types ascolimits of a family of approximations to them defined by well-foundedrecursion over a suitable notion of size, whose definition involves the WISCaxiom. We developed the proof and checked it using the Agda theorem prover