Abstract: Traditional methods including category theory and coalgebra have some drawbacks to analyze semantic    behavior and describe co-inductive rule, this paper explores indexed co-inductive data type (ICDT) in programming by Fibrations theory. Firstly, this paper constructs indexed Fibration by change of base, presents some tools such as equation functor and quotient functor of indexed Fibration, and then analyzes deeply semantic behavior of ICDT by adjunction property and lifting equation-preserving. Based on this, this paper proposes a parameterized co-recursive operation on ICDT to describe abstractly co-inductive rule with universality in the framework of Fibrations theory, also briefly introduces applications of Fibrations theory for ICDT by example. Compared with traditional methods, brief descriptions and flexible expansibility of Fibrations theory can analyze semantic behavior of ICDT accurately, its superior abstractness doesn't rely on particular computing environments to describe co-inductive rule with universality of ICDT.

Key words: semantic behavior, co-induction rule, change of base, lifting, co-recursion

摘要： 传统范畴论与共代数等方法在分析语义行为与描述共归纳规则方面存在不足，应用Fibrations理论对程序语言中索引共归纳数据类型（indexed co-inductive data type，ICDT）进行了研究。通过基变换构造索引Fibration，建立索引Fibration的等式函子与商函子等工具，应用伴随性质与保持等式的提升深入分析ICDT的语义行为；以此为基础，构造ICDT上参数化的共递归操作，在Fibrations理论框架内抽象描述具有普适意义的共归纳规则，并以实例分析简要介绍Fibrations理论在ICDT中的应用。与传统研究方法相比，Fibrations理论具有简洁的描述性与灵活的扩展性，可以精确分析ICDT的语义行为，具有高度的抽象性且不依赖特定的计算环境，描述了ICDT具有普适意义的共归纳规则。

关键词: 语义行为, 共归纳规则, 基变换, 提升, 共递归