Abstract: Traditional methods of co-inductive data types in programming,such as co-algebra and category theory,have some problems in analyzing semantics behaviors and describing co-inductive rules.Considering the status quo of co-inductive data types researches both at home and abroad,a fibrations method was proposed in this paper.Firstly, some basic logical structures of co-inductive data types are systematically analyzed over a fibration including reindexed functor,op-reindexed functor and truth functor,and the corresponding relationship between co-inductive data types and their semantic behaviors on program logic is established by equality functor and quotient functor.Then semantic behaviors of co-inductive data types are deeply analyzed .Secondly, co-recursive operations are constructed to describe abstractly co-inductive rules of co-inductive data types with universality by endo-functors in base categories and their equality-preserving lifting in total categories.At last applications of fibrations method are briefly introduced by examples.

Key words: Semantic behaviors,Co-inductive rules,Fibrations method,Co-inductive data types,Lifting