一句话：通过签名理论构造有限QIIT，并证明其存在、依赖消去及与初始代数等价
商归纳-归纳类型（QIIT）从两方面推广归纳类型：可有多个排序，且后续排序可依赖前面的排序；此外还允许相等构造子。在满足同一性证明唯一性（UIP）的设定下，本文称之为 QIIT。典型例子是经转换商化的良类型内在语法。本文首先用称为签名理论的领域特定类型论来刻画有限 QIIT，而签名理论自身的语法也由 QIIT 给出。基于该语法，作者证明所有被刻画的 QIIT 均存在并具有依赖消去原理；还证明一个签名的代数构成依赖族范畴（CwF），并利用该 CwF 的内部语言证明依赖消去与初始性等价。
Quotient inductive-inductive types (QIITs) generalise inductive types in two ways: a QIIT can have more than one sort and the later sorts can be indexed over the previous ones. In addition, equality constructors are also allowed. We work in a setting with uniqueness of identity proofs, hence we use the term QIIT instead of higher inductive-inductive type. An example of a QIIT is the well-typed (intrinsic) syntax of type theory quotiented by conversion. In this paper first we specify finitary QIITs using a domain-specific type theory which we call the theory of signatures. The syntax of the theory of signatures is given by a QIIT as well. Then, using this syntax we show that all specified QIITs exist and they have a dependent elimination principle. We also show that algebras of a signature form a category with families (CwF) and use the internal language of this CwF to show that dependent elimination is equivalent to initiality.
@article{paperbot618,
title = {Constructing quotient inductive-inductive types},
author = {Ambrus Kaposi and András Kovács and Thorsten Altenkirch},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290315}
}