Indexed Induction And Coinduction, Fibrationally

ASU Author/Contributor (non-ASU co-authors, if there are any, appear on document)
Patricia Johann Ph.D, Professor (Creator)
Appalachian State University (ASU )
Web Site:

Abstract: This paper extends the fibrational approach to induction and coinductionpioneered by Hermida and Jacobs, and developed by the current authors, in two keydirections. First, we present a dual to the sound induction rule for inductive types thatwe developed previously. That is, we present a sound coinduction rule for any data typearising 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 quotientcategory with equality (QCE) that i) abstracts the standard notion of a fibration of relationsconstructed from a given fibration; and ii) plays a role in the theory of coinduction dualto 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 inductionand coinduction rules. Indexed data types often arise as carriers of initial algebras andfinal coalgebras of functors on slice categories, so we give sufficient conditions under which we can construct, from a CCU (QCE) U : E : 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 themore general case of sound induction and coinduction rules for indexed data types whenthe indexing is itself given by a fibration.

Additional Information

Neil Ghani , Patricia Johann, and Clement Fumex(2013) Indexed Induction and Coinduction, Fibrationally. Logical Methods in Computer Science vol.9(3:6) pp 1-31 Version of record available at (
Language: English
Date: 2013
induction, coinduction, fibrations,

Email this document to