Structural induction and coinduction in a fibrational setting (Q1275820)

A categorical logic formulation of induction and coinduction is proposed. The main results provide criteria for the validity of such principles: in the presence of comprehension, the induction principle for initial algebras is admissible, and in the presence of quotient types, the coinduction principle for terminal coalgebras is admissible. One of the main points is to give formulation, in a canonical fashion, of an induction principle for initial algebras and a coinduction principle for terminal coalgebras using polynomial functors. The results on validity of the induction and coinduction principles (main results of the paper) are presented as admissibility properties of constructive predicate logic. Using this, the authors give a reasoning principle for recursive data types involving mixed variance functors. The connections with contextual and functional completeness, internal full abstraction, adequacy and strong extensionality are considered. It is argued that the level of abstraction achieved in the paper is the right level of abstraction to combine salient features of the above approaches.