Sciweavers

CALCO
2011
Springer

Indexed Induction and Coinduction, Fibrationally

12 years 3 months ago
Indexed Induction and Coinduction, Fibrationally
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 sound coinduction rule for any data type arising as the final coalgebra of a functor, thus relaxing Hermida and Jacobs’ restriction to polynomial data types. For this we introduce the notion of a quotient category with equality (QCE), which tracts the standard notion of a fibration of relations constructed from a given fibration, and plays a role in the theory of coinduction dual to that of a comprehension category with unit (CCU) in the theory of induction. Second, we show that indexed inductive and coinductive types also admit sound induction and coinduction rules. Indexed data types often arise as initial algebras and final coalgebras of functors on slice categories, so our key technical results give sufficent conditions under which we can construct, from a CCU (QCE) U : E → B, a fibration...
Clément Fumex, Neil Ghani, Patricia Johann
Added 13 Dec 2011
Updated 13 Dec 2011
Type Journal
Year 2011
Where CALCO
Authors Clément Fumex, Neil Ghani, Patricia Johann
Comments (0)