Indexed Induction and Coinduction, Fibrationally

TL;DR

This paper advances fibrational methods for induction and coinduction by introducing a dual coinduction rule applicable to all data types as final coalgebras, and extends these rules to indexed types using quotient categories and fibrations.

Contribution

It introduces a dual to the induction rule for coinductive types, relaxing previous restrictions, and develops sound induction and coinduction rules for indexed data types within a fibrational framework.

Findings

Developed a sound coinduction rule for all data types as final coalgebras.

Extended induction and coinduction rules to indexed data types.

Introduced quotient categories with equality (QCE) for coinduction.

Abstract

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.