一句话：在构造类型论中引入 QWI 类型，并证明其可由商类型与归纳类型导出，Agda 机器化验证。
本文在构造类型论中引入一类带索引的商归纳类型（QWI 类型），它是一族可能含无穷算子与方程的等式理论的初始代数。作者证明：在具有自然数对象和宇宙的 topos 类型论中，若宇宙满足弱初始覆盖集（WISC）公理，则 QWI 类型可由商类型与归纳类型导出。构造方法是将 QWI 类型表示为一系列近似项的余极限，这些近似通过基于合适大小概念的良基递归定义，其中 WISC 公理用于保证覆盖族的存在。证明已在 Agda 证明助手中形式化检查。
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.
@article{paperbot1696,
title = {Quotients, inductive types, and quotient inductive types},
author = {Marcelo P. Fiore and Andrew M. Pitts and S. C. Steenkamp},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 2},
year = {2022},
doi = {10.46298/lmcs-18(2:15)2022}
}