纤维化视角下的索引归纳与共归纳

本文在两个关键方向上扩展了由 Hermida 和 Jacobs 开创并由当前作者发展的关于归纳与共归纳的纤维化方法。首先，我们提出了我们之前开发的针对归纳类型的可靠归纳规则的对偶形式。也就是说，我们为任何作为函子终余代数载体的数据类型提出了一个可靠的共归纳规则，从而放宽了 Hermida 和 Jacobs 对多项式函子的限制。为此，我们引入了具有相等性的商范畴 (quotient category with equality, QCE) 的概念，该概念 i) 抽象了从给定纤维化构造的关系纤维化的标准概念；ii) 在共归纳理论中扮演的角色，类似于带有单位的理解范畴 (comprehension category with unit, CCU) 在归纳理论中所扮演的角色。其次，我们证明了索引归纳类型和索引共归纳类型也允许可靠的归纳和共归纳规则。索引数据类型通常作为切片范畴上函子的初始代数和终余代数的载体出现，因此我们给出了充分条件，在这些条件下，我们可以从 CCU (QCE) $U:E \rightarrow B$ 构造一个以 $B/I$ 为底的纤维化，该纤维化模拟由 $I$ 进行的索引，并且本身也是一个 CCU（分别为 QCE）。最后，我们考虑了更一般的情况，即当索引本身由纤维化给出时，索引数据类型的可靠归纳和共归纳规则。