一句话：为大型与无穷 QIIT 建立元理论，并用 CwF 代数模型给出语义。
商归纳-归纳类型（QIITs）允许排序索引于先前声明的排序，并可使用等式构造子，常用于类型论的代数描述及实数、序数、超现实数的构造性定义。本文为其扩展出支持大型（large）QIIT、大型消去、递归方程与无穷构造子的新元理论。作者沿用“每个语境表示一个 QIIT 签名”的类型论思路，但使签名理论能够在宇宙大小限制下描述自身；通过自描述与 Church 编码的签名概念自举模型论，避免复杂原始语法或假定内部 QIIT 签名。语义上，每个签名被建模为代数上的有限完备 CwF，并用 isofibration 处理代数同构不变性。最后以项模型构造证明每个 QIIT 都可从签名理论语法构造。
Quotient inductive-inductive types (QIITs) are generalized inductive types which allow sorts to be indexed over previously declared sorts, and allow usage of equality constructors. QIITs are especially useful for algebraic descriptions of type theories and constructive definitions of real, ordinal and surreal numbers. We develop new metatheory for large QIITs, large elimination, recursive equations and infinitary constructors. As in prior work, we describe QIITs using a type theory where each context represents a QIIT signature. However, in our case the theory of signatures can also describe its own signature, modulo universe sizes. We bootstrap the model theory of signatures using self-description and a Church-coded notion of signature, without using complicated raw syntax or assuming an existing internal QIIT of signatures. We give semantics to described QIITs by modeling each signature as a finitely complete CwF (category with families) of algebras. Compared to the case of finitary QIITs, we additionally need to show invariance under algebra isomorphisms in the semantics. We do this by modeling signature types as isofibrations. Finally, we show by a term model construction that every QIIT is constructible from the syntax of the theory of signatures.