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.

翻译：本文在建设性类型理论的框架内,引入了称为QWI类型的指数式感知型类。它们是对等理论的指数式系的初始代数,可能具有无限操作者和方程。我们证明,QWI类型可以来自自然编号对象和宇宙的参数类型和感知型,前提是这些宇宙满足了最弱的初始覆盖体(WISC)xiom。我们这样做的方式是将QWI类型构建成一个近似体系的共限,其定义是有充分根据的重现,其定义涉及适当的大小概念,其定义涉及WISC exiom。我们用Agda Theorem 证明书开发了证据并检查了证据。