  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.
