指数诱导和共诱导，纤维化
Indexed Induction and Coinduction, Fibrationally
摘要：
本文扩展了纤维化的方法，以诱导和coinductive开创了Hermida和雅各布斯，并开发了目前的作者，在两个关键的方向。首先，我们提出了一个对偶的归纳类型，我们以前开发的健全的归纳规则。也就是说，我们提出了一个健全的共归纳规则的任何数据类型出现的载体的最后一个函子的余代数，从而放松Hermida和雅各布斯的限制多项式函子。为了实现这一点，我们引入了具有相等性的商范畴（QCE）的概念，它i）抽象了从给定纤维化构造的关系的纤维化的标准概念; ii）在共归纳理论中起着与归纳理论中具有单位的理解范畴（CCU）对偶的作用。其次，我们表明，归纳和共归纳索引类型也承认健全的归纳和共归纳规则。索引数据类型通常作为切片范畴上函子的初始代数和最终余代数的载体出现，因此我们给出了充分条件，在此条件下，我们可以从CCU（QCE）U：E \rightarrow B构造具有基B/I的纤维化，该纤维化以I为索引模型，并且也是CCU（分别为，QCE）。我们完成的文件，考虑更一般的情况下，健全的归纳和coinduction规则的索引数据类型时，索引本身是由纤维化。
英文摘要：
This paper extends the fibrational approach to induction and coinduction pioneered by Hermida and Jacobs, and developed by the current authors, in two key directions. First, we present a dual to the sound induction rule for inductive types that we developed previously. That is, we present a sound coinduction rule for any data type arising as the carrier of the final coalgebra of a functor, thus relaxing Hermida and Jacobs' restriction to polynomial functors. To achieve this we introduce the notion of a quotient category with equality (QCE) that i) abstracts the standard notion of a fibration of relations constructed from a given fibration; and ii) plays a role in the theory of coinduction dual to that played by a comprehension category with unit (CCU) in the theory of induction. Secondly, we show that inductive and coinductive indexed types also admit sound induction and coinduction rules. Indexed data types often arise as carriers of initial algebras and final coalgebras of functors on slice categories, so we give sufficient conditions under which we can construct, from a CCU (QCE) U:E \rightarrow B, a fibration with base B/I that models indexing by I and is also a CCU (resp., QCE). We finish the paper by considering the more general case of sound induction and coinduction rules for indexed data types when the indexing is itself given by a fibration.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
