商、归纳类型与商归纳类型
摘要：基于构造型理论，本文介绍了一种表达力强的索引商多样式，称为QWI类型。它们是索引等式理论的初始代数，其中可能包含无限的运算符和等式。我们证明了QWI类型可以从商类型和归纳类型中派生出来，在带有自然数对象和宇宙的拓扑学类型理论中成立，前提是这些宇宙满足弱初始覆盖集（WISC）公理。我们通过构造QWI类型作为逼近它们的一个族系的余极限来实现这一点，该族系的定义通过基于某种大小概念上的良基递归来完成，其定义包括WISC公理。我们使用Agda定理证明器开发了证明并对其进行了验证。
作者：Marcelo P. Fiore and Andrew M. Pitts and S. C. Steenkamp
论文ID：2101.02994
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22