STRUCTURAL INDUCTION AND COINDUCTION IN A FIBRATIONAL SETTING

We present a categorical logic formulation of induction and coinductio n principles for reasoning about inductively and coinductively defined types. Our main results provide sufficient criteria for the validity of such principles: in the presence of comprehension, the induction pr inciple for initial algebras is admissible, and dually, in the presenc e of quotient types, the coinduction principle for terminal coalgebras is admissible. After giving an alternative formulation of induction i n terms of binary relations, we combine both principles and obtain a m ixed induction/coinduction principle which allows us to reason about m inimal solutions X congruent to sigma(X) where X may occur both positi vely and negatively in the type constructor sigma. We further strength en these logical principles to deal with contexts and prove that such strengthening is valid when the (abstract) logic we consider is contex tually/functionally complete. All the main results follow from a basic result about adjunctions between ''categories of algebras'' (inserter s). (C) 1998 Academic Press.